| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
Also remove a rewrite rule using cast from the non-cast arith rules,
regenerate the .out files, add ident.gets_inlined for eventual use in
the rewriter, and generalize the rewrite rule lemmas over
cast_out_of_range so that we can actually make use of their proofs for
interp.
|
| |
|
| |
|
|
|
|
|
|
| |
Actually useful ones, this time
Constructed with much pain and some trial-and-error and guessing.
|
|
|
|
|
|
|
|
| |
Rather than using Forall2 in some places and a combination of length,
combine, and In in others, we now primarily use Forall2.
There is probably some dead tactic code as a result of this that I just
haven't bothered to clean up.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This is needed to reify statements for the rewriter.
|
|
|
|
| |
These will be useful for extending the AST with `option` types.
|
|
|