aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* WIPGravatar jadep2019-03-25
* Add UnderLets.wf_flat_mapGravatar Jason Gross2019-03-12
* Add UnderLets.wf_of_exprGravatar Jason Gross2019-03-09
* Add some UnderLets wf proofsGravatar Jason Gross2019-03-08
* Standardize list wf thingsGravatar Jason Gross2019-03-08
* Add Forall2_Proper instancesGravatar Jason Gross2019-03-08
* Add Forall2_map_map_iffGravatar Jason Gross2019-03-08
* Add wf_reify_list_Forall2Gravatar Jason Gross2019-03-08
* Allow more reucrsion in wf_safe_t_stepGravatar Jason Gross2019-03-08
* Fix issue with previous commitGravatar Jason Gross2019-03-08
* Add some eq list_rect lemmas to ListUtilGravatar Jason Gross2019-03-08
* Add eager_nth_defaultGravatar Jason Gross2019-03-08
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Fix grepeat tacticGravatar Jason Gross2019-03-08
* Fix gprogress tacticalGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Fix a typoGravatar Jason Gross2019-03-08
* add wf_smart_Literal_eqGravatar Jason Gross2019-03-08
* Add wf_smart_LiteralGravatar Jason Gross2019-03-08
* Add Forall2_forall_In_combine_iffGravatar Jason Gross2019-03-07
* Add wf proofs to UnderLetsProofsGravatar Jason Gross2019-03-07
* Fix hypothesis of UnderLets.list_rect_arrow_interp_relatedGravatar Jason Gross2019-03-07
* Add UnderLets.list_rect_arrow_interp_relatedGravatar Jason Gross2019-03-07
* Add some eq lemmas to ListUtilGravatar Jason Gross2019-03-07
* 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
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
* Update .out filesGravatar Jason Gross2019-03-07
* Reify most rewrite rulesGravatar Jason Gross2019-03-07
* Fix reification of interpreted identsGravatar Jason Gross2019-03-06
* Add support for reifying fancy identifiersGravatar Jason Gross2019-03-06
* Add reserved notations for \inGravatar Jason Gross2019-03-05
* Allow reifying Z.cast2Gravatar Jason Gross2019-03-05
* Fix unfolding of pattern.base.lookup_defaultGravatar 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
* Add UnderLets.flat_mapGravatar Jason Gross2019-03-05
* Fix another instance of reductionGravatar Jason Gross2019-03-04
* Fix reductionGravatar Jason Gross2019-03-04
* Fix an issue with a proof from the previous commitGravatar Jason Gross2019-03-04
* Add some things to GENERATED rewriter fileGravatar Jason Gross2019-03-04
* Allow reifying cast and literalsGravatar Jason Gross2019-03-04
* Add some minor reflect thingsGravatar Jason Gross2019-03-04
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Update a proof to work with previous commitGravatar Jason Gross2019-02-27
* Add UnderLets.mapGravatar Jason Gross2019-02-27
* finish porting barrett and montgomery code to new glue styleGravatar jadep2019-02-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-20 13:33:00 +0000