aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Minor change to reflection namingGravatar Jason Gross2017-02-23
* Add various reflection improvements, boundbycastGravatar Jason Gross2017-02-21
* Add interpf_smart_bound without exprfGravatar Jason Gross2017-02-21
* Rename Interp lemmasGravatar Jason Gross2017-02-21
* Add non-exprf version of interpf_smart_unboundGravatar Jason Gross2017-02-16
* Add MapCastInterpGravatar Jason Gross2017-02-16
* Add InterpByIsoProofsGravatar Jason Gross2017-02-16
* Fix typoGravatar Jason Gross2017-02-16
* Add InterpByIsoGravatar Jason Gross2017-02-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 08:09:15 +0000