| Age | Commit message (Collapse) | Author |
|---|
|
multiple arguments weren't type-checking correctly
|
|
|
|
|
|
|
|
isabelle (but isabelle almost certainly broken)
|
|
correctly
|
|
|
|
riscv model.
|
|
|
|
This means that a mapping which formerly had to be pre-declared like
val name : a <-> b
...
mapping name {
x <-> y,
...
}
can now be shortened to
mapping name : a <-> b {
x <-> y,
...
}
|
|
|
|
|
|
stuff now compiles to Lem
|
|
|
|
exception. This should fix the sbreak test.
|
|
|
|
pass.
|
|
|
|
|
|
|
|
|
|
|
|
Also add test cases and Isabelle lemmas
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Mostly introducing type variables for regsize in valspecs
|
|
(should really make the Lem pretty printer use the solver properly,
but this is a useful stopgap)
|
|
|
|
|
|
|
|
The pattern types may be subtypes, using those caused it to try rewriting
int parameters and failing
|
|
|
|
Replace the old manual with new version in repository root
|
|
|
|
|
|
Should have all the main language features covered in at least some
detail now.
|
|
"sum" is an existing constant in Isabelle, and the Lem constant avoiding
mechanism does not seem to pick it up when used as the name of a function
parameter.
|
|
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
|
|
|
|
|
|
|
