aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Add invert_match_exprGravatar Jason Gross2017-02-01
* Add invert_exprGravatar Jason Gross2017-02-01
* Add wff_SmartVarVarf_nilGravatar Jason Gross2017-02-01
* 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
* Add flatten_binding_list_SmartValfGravatar Jason Gross2017-01-24
* Add SmartFlatTypeUnMapGravatar Jason Gross2017-01-24
* Add flatten_binding_list_SmartVarfMapGravatar Jason Gross2017-01-24
* Add SmartVarf{Type,Prop}Map{,2}Gravatar Jason Gross2017-01-24
* Add SmartVarfMap_idGravatar Jason Gross2017-01-24
* Add SmartVarfMap2Gravatar Jason Gross2017-01-24
* Add smart_interp_flat_map2Gravatar Jason Gross2017-01-24
* Add match commutation lemmasGravatar Jason Gross2017-01-23
* Preserve names in invert_expr_substGravatar Jason Gross2017-01-23
* Make invert_expr_subst not loopGravatar Jason Gross2017-01-23
* Fix invert_expr_substGravatar Jason Gross2017-01-23
* Better invert_exprGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Fix a typoGravatar Jason Gross2017-01-23
* Add invert_expr_substGravatar Jason Gross2017-01-23
* Allow inversion on wff if either side is not a varGravatar Jason Gross2017-01-23
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
* Revert "Fix a missing qualification"Gravatar Jason Gross2017-01-21
* Fix a missing qualificationGravatar Jason Gross2017-01-21
* Move weqb_hetero to Bedrock.WordGravatar Jason Gross2017-01-21
* Add weqb_heteroGravatar Jason Gross2017-01-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-10 04:32:41 +0000