Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix for 8.8 | Jason Gross | 2019-04-05 |
| | |||
* | Add interp_related lemmas | Jason Gross | 2019-04-05 |
| | |||
* | Add some more underlets lemmas | Jason Gross | 2019-04-04 |
| | |||
* | Add UnderLets flat_map interp proofs,other changes | Jason Gross | 2019-04-04 |
| | | | | | | | | 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. | ||
* | Add UnderLets.wf_flat_map | Jason Gross | 2019-03-12 |
| | |||
* | Add UnderLets.wf_of_expr | Jason Gross | 2019-03-09 |
| | |||
* | Add some UnderLets wf proofs | Jason Gross | 2019-03-08 |
| | | | | | | Actually useful ones, this time Constructed with much pain and some trial-and-error and guessing. | ||
* | Standardize list wf things | Jason Gross | 2019-03-08 |
| | | | | | | | | 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. | ||
* | Add wf proofs to UnderLetsProofs | Jason Gross | 2019-03-07 |
| | |||
* | Fix hypothesis of UnderLets.list_rect_arrow_interp_related | Jason Gross | 2019-03-07 |
| | |||
* | Add UnderLets.list_rect_arrow_interp_related | Jason Gross | 2019-03-07 |
| | |||
* | Update a proof to work with previous commit | Jason Gross | 2019-02-27 |
| | |||
* | Add support for reifying `zrange` and `option` | Jason Gross | 2019-02-18 |
| | | | | This is needed to reify statements for the rewriter. | ||
* | Add Option.{lift,map,combine}, List.Option.lift | Jason Gross | 2019-02-11 |
| | | | | These will be useful for extending the AST with `option` types. | ||
* | move src/Experiments/NewPipeline/ to src/ | Andres Erbsen | 2019-01-09 |