aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Added saturated arithmetic file, including [compact] code and proofGravatar jadep2017-03-24
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
* Fix binder counting in MapCastByDBGravatar Jason Gross2017-03-22
* Add aborted CompilePropertiesGravatar Jason Gross2017-03-22
* Add split_onames_split_namesGravatar Jason Gross2017-03-22
* Add length_fst_split_names_None_iffGravatar Jason Gross2017-03-22
* Also count lets in operations and pairsGravatar Jason Gross2017-03-22
* Add length_fst_split_names_Some_iffGravatar Jason Gross2017-03-22
* Fix MapCastByDeBruijnInterpGravatar Jason Gross2017-03-22
* Prove that mapf_cast gives the correct boundsGravatar Jason Gross2017-03-22
* Add debug output for success in reifyfGravatar Jason Gross2017-03-22
* Add cast_back_flat_constGravatar Jason Gross2017-03-22
* Split off extra power of ltb_to_lt, split_andbGravatar Jason Gross2017-03-21
* Remove a line I forgot to remove in the previous commitGravatar Jason Gross2017-03-21
* Split off the extra power of rewrite_mod_small into rewrite_mod_mod_smallGravatar Jason Gross2017-03-21
* Make Z.rewrite_mod_small a bit more powerfulGravatar Jason Gross2017-03-21
* Make Bool.split_andb a bit more powerfulGravatar Jason Gross2017-03-21
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
* Add aborted MapCastByDeBruijnWfGravatar Jason Gross2017-03-19
* Finish MapCastCorrectGravatar Jason Gross2017-03-19
* Add more to CompileWfGravatar Jason Gross2017-03-19
* Add MapCastWfGravatar Jason Gross2017-03-19
* Most of the way towards a complete MapCastCorrectGravatar Jason Gross2017-03-19
* Add Named/PositiveContext/DefaultsProperties.vGravatar Jason Gross2017-03-19
* Add {firstn,skipn}_seqGravatar Jason Gross2017-03-19
* Finish CompileInterp proofGravatar Jason Gross2017-03-19
* Split up ContextPropertiesGravatar Jason Gross2017-03-19
* Add mname_list_unique_nilGravatar Jason Gross2017-03-19
* Add more ContextPropertiesGravatar Jason Gross2017-03-19
* generalize In_firstn_skipn_splitGravatar Jason Gross2017-03-19
* Add In_firstn_skipn_splitGravatar Jason Gross2017-03-19
* Add {m,o,}name_list_uniqueGravatar Jason Gross2017-03-19
* Add firstn_firstn_minGravatar Jason Gross2017-03-19
* Add Addmitted correctness for MapCastByDeBruijnGravatar Jason Gross2017-03-19
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
* Minor simplification in SmartBoundGravatar Jason Gross2017-03-18
* Add dec_eq_positiveGravatar Jason Gross2017-03-17
* Switch to more robust automation in MapCastInterpGravatar Jason Gross2017-03-17
* Add default_names_for{,f}Gravatar Jason Gross2017-03-17
* Add IdContextGravatar Jason Gross2017-03-17
* Revert "Have cast_op return exprf instead of op"Gravatar Jason Gross2017-03-17
* Have cast_op return exprf instead of opGravatar Jason Gross2017-03-17
* Add MapCastByDeBruijn on PHOAS syntaxGravatar Jason Gross2017-03-17
* Don't pass a wf proof into InterpToPHOASGravatar Jason Gross2017-03-17
* Add aborted in-process compile-{wf,interp} proofsGravatar Jason Gross2017-03-17
* Add a Named version of MapCastGravatar Jason Gross2017-03-17
* Fix a name clashGravatar Jason Gross2017-03-14
* Add split_{m,o,}names_firstn_skipn and co.Gravatar Jason Gross2017-03-14
* Add firstn_skipnGravatar Jason Gross2017-03-14
* Add split_prodGravatar Jason Gross2017-03-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 03:43:27 +0000