aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
* Remove useless commentGravatar Jason Gross2017-02-14
* Mostly finish Wf_BoundifyGravatar Jason Gross2017-02-14
* Prove wff_bound_opGravatar Jason Gross2017-02-14
* Stub for wff_bound_opGravatar Jason Gross2017-02-14
* Add Wf_MapInterpCast to wf databaseGravatar Jason Gross2017-02-14
* A bit more progress on BoundByCastWfGravatar Jason Gross2017-02-14
* Add partially finished MapCastWfGravatar Jason Gross2017-02-14
* Add src/Reflection/BoundByCastWf.vGravatar Jason Gross2017-02-14
* Update assumptions in src/Reflection/SmartBoundWf.vGravatar Jason Gross2017-02-14
* Add SmartBoundWfGravatar Jason Gross2017-02-14
* Prove nicer version of wf_SmartAbsGravatar Jason Gross2017-02-13
* Add partially admitted lemma wf_SmartAbsGravatar Jason Gross2017-02-13
* More uniform namingGravatar Jason Gross2017-02-13
* Generalize EtaWf some (still one admit)Gravatar Jason Gross2017-02-13
* Add InlineCastInterp.vGravatar Jason Gross2017-02-13
* Add InlineCastWfGravatar Jason Gross2017-02-13
* Better cleanup in type_inversionGravatar Jason Gross2017-02-13
* Better type_inversionGravatar Jason Gross2017-02-13
* Split off inversion_wff for constr-only hypsGravatar Jason Gross2017-02-13
* Add inversion_typeGravatar Jason Gross2017-02-13
* Generalize InlineWfGravatar Jason Gross2017-02-13
* Add SmartCast{Interp,Wf}Gravatar Jason Gross2017-02-13
* Split up BoundByCastGravatar Jason Gross2017-02-13
* Generalize BoundByCast a bitGravatar Jason Gross2017-02-10
* Add EtaInterp, EtaWfGravatar Jason Gross2017-02-10
* Use Eta in BoundByCastGravatar Jason Gross2017-02-10
* Add Reflection/Eta.vGravatar Jason Gross2017-02-10
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* Remove useless importsGravatar Jason Gross2017-02-08
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* Fix type inference bug in 8.6Gravatar Jason Gross2017-02-08
* Simpler version of MapCastGravatar Jason Gross2017-02-08
* Remove the let-in from SmartValfGravatar Jason Gross2017-02-07
* Fix relation relb argumentsGravatar Jason Gross2017-02-07
* Add things like interp_flat_type_rel_pointwise1_gen_Prop_iff_boolGravatar Jason Gross2017-02-07
* Clean up and improve Reflection.RelationsGravatar Jason Gross2017-02-07
* Add interp_flat_type_rel_pointwise2_flatten_binding_listGravatar Jason Gross2017-02-06
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
* Add interp_flat_type_rel_pointwise2_hetero_iffGravatar 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 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 03:06:12 +0000