aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
* Factor out rewriter rulesGravatar Jason Gross2019-03-31
* Fix a non-terminated commentGravatar Jason Gross2019-03-31
* Add some comments based on CR requestsGravatar Jason Gross2019-03-31
* Fix issue with refolding in eapply in < 8.9Gravatar Jason Gross2019-03-31
* Finish reifying list lemmasGravatar Jason Gross2019-03-31
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* improve zero_bounds tacticGravatar jadep2019-03-26
* add some hints to the global databasesGravatar jadep2019-03-26
* remove Derive to fix 8.7Gravatar jadep2019-03-25
* fix montgomeryGravatar jadep2019-03-25
* remove 2: syntax so I don't break 8.7Gravatar jadep2019-03-25
* fix up a messy proofGravatar jadep2019-03-25
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
* finish proofsGravatar jadep2019-03-25
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 04:42:24 +0000