aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Also unfold wcmovl, wcmovne, wneg in fixed_size_constantsGravatar Jason Gross2017-02-03
* Don't autounfold wordToZ nor ZToWordGravatar Jason Gross2017-02-03
* Add fixed_size_op_to_word tacticGravatar Jason Gross2017-02-03
* Add interp_flat_type_rel_pointwise2_hetero_iffGravatar Jason Gross2017-02-03
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
* Reorder Reflection.Z.SyntaxGravatar Jason Gross2017-02-02
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Add wf databaseGravatar Jason Gross2017-02-01
* Generalize InlineInterpGravatar Jason Gross2017-02-01
* Fix lazymatch orderingGravatar Jason Gross2017-02-01
* More powerful preinvert_one_typeGravatar Jason Gross2017-02-01
* Add wordToZ_ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add ZToWord_wordToZ_ZToWordGravatar Jason Gross2017-02-01
* Add NToWord_wordToN_NToWordGravatar Jason Gross2017-02-01
* Add wordToZ_ZToWord, ZToWord_wordToZGravatar Jason Gross2017-02-01
* Add invert_match_opGravatar Jason Gross2017-02-01
* Add invert_opGravatar Jason Gross2017-02-01
* Add inversion_exprGravatar Jason Gross2017-02-01
* Add invert_match_exprGravatar Jason Gross2017-02-01
* Add invert_exprGravatar Jason Gross2017-02-01
* Add wff_SmartVarVarf_nilGravatar Jason Gross2017-02-01
* Bump submodule for better travis timing logsGravatar Jason Gross2017-01-31
* Preferentially invert wff with two constructorsGravatar Jason Gross2017-01-31
* Absolutize some importsGravatar Jason Gross2017-01-31
* Absolutize some importsGravatar Jason Gross2017-01-31
* Nicer inversion_wffGravatar Jason Gross2017-01-31
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Fix implicitsGravatar Jason Gross2017-01-31
* Add SmartFlatTypeMap2Interp2Gravatar Jason Gross2017-01-31
* Don't change sumbool eq hypothesis unless both sides are constructorsGravatar Jason Gross2017-01-30
* Fix typosGravatar Jason Gross2017-01-30
* Add Util.SumboolGravatar Jason Gross2017-01-30
* Add inversion_flat_type, inversion_typeGravatar Jason Gross2017-01-30
* Add In_G_wff_SmartVarf, SmartVarf_PairGravatar Jason Gross2017-01-30
* Add interp_flat_type_rel_pointwise0Gravatar Jason Gross2017-01-27
* Better typing for SmartPairf_PairGravatar Jason Gross2017-01-27
* Remove dead codeGravatar Jason Gross2017-01-27
* Add SmartPairf_PairGravatar Jason Gross2017-01-27
* Doc fixupGravatar Jason Gross2017-01-27
* Various minor reflection fixupsGravatar Jason Gross2017-01-27
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Add interp_type_rel_pointwise2_heteroGravatar Jason Gross2017-01-25
* Add interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add flatten_binding_list2_SmartVarfMap{1,2}Gravatar Jason Gross2017-01-25
* Lemmas about flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add flatten_binding_list2Gravatar Jason Gross2017-01-25
* Add interp_flat_type_rel_pointwise2_heteroGravatar Jason Gross2017-01-25
* Generalize flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:28:02 +0000