| Age | Commit message (Collapse) | Author |
|---|
|
Refine types of primitive functions to permit more constraints to be properly checked.
|
|
declared return type when consistent instead of using the derived one.
|
|
|
|
|
|
|
|
|
|
|
|
(make one function to do it instead of almost the same function multiple times)
Fix lost nexp variable in constraints, removing another undefined
|
|
|
|
|
|
|
|
call to turn them positive, in to_vec*
|
|
|
|
|
|
|
|
decoding an ARM instruction.
(Note: may fix issue #2, haven't checked yet)
|
|
theorem provers, use structural (in)equality for Isabelle and HOL for literals and values
|
|
|
|
being very power-specific.
Note: slight interface change to instruction_extractor
|
|
|
|
|
|
|
|
|
|
numbers (explicit instead of implicit in operations)
|
|
|
|
|
|
And fix match failure problem (hopefully)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
|
|
|
|
|
|
increasing while supporting inc and dec views to the interpreter and in printing
Fix bugs exposed by running idlarm several instructions (after fixing above)
|
|
|
|
|
|
where they shouldn't be
|
|
|
|
|
|
|
|
|
|
|
|
of type nat (at least not without a >= 0 check)
|
|
|
|
Fix up parsing on 2** precedence
Fix errors on type variables in function definition
|
|
|
