aboutsummaryrefslogtreecommitdiff
path: root/src/Language.v
Commit message (Expand)AuthorAge
* Automate more of the rewriter, and factor out rule-specific thingsGravatar Jason Gross2019-04-11
* Add base.reflect_{base,type}_beq and type.reflect_type_beqGravatar Jason Gross2019-04-10
* Add UnderLets flat_map interp proofs,other changesGravatar Jason Gross2019-04-04
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Add eager_nth_defaultGravatar Jason Gross2019-03-08
* Also reify List.mapGravatar Jason Gross2019-03-07
* Add list_rect_arrowGravatar Jason Gross2019-03-07
* Add a couple more identifiers to support eager recGravatar Jason Gross2019-03-07
* Fix reification of interpreted identsGravatar Jason Gross2019-03-06
* Add support for reifying fancy identifiersGravatar Jason Gross2019-03-06
* Allow reifying Z.cast2Gravatar Jason Gross2019-03-05
* Actually fix reification of literalsGravatar Jason Gross2019-03-05
* Revert "Fix reification of literals"Gravatar Jason Gross2019-03-05
* Fix reification of literalsGravatar Jason Gross2019-03-05
* Allow reifying cast and literalsGravatar Jason Gross2019-03-04
* Add base.{base_,}interp_beqGravatar Jason Gross2019-02-20
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
* Actually support Nat.eqb in reificationGravatar Jason Gross2019-01-25
* Support Nat.eqb in reificationGravatar Jason Gross2019-01-25
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09