aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Add more display logsGravatar Jason Gross2017-02-16
* Fix typoGravatar Jason Gross2017-02-16
* Add InterpByIsoGravatar Jason Gross2017-02-16
* Add more display logsGravatar Jason Gross2017-02-15
* Add some display logsGravatar Jason Gross2017-02-15
* Add some display logsGravatar Jason Gross2017-02-15
* ./copy_boundsGravatar Jason Gross2017-02-15
* 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
* Fix a missing section close in ZToRingGravatar Jason Gross2017-02-10
* Add files for constant reflective notationsGravatar Jason Gross2017-02-10
* Accidentally pushed wrong file in last commit; this is the correct oneGravatar jadep2017-02-10
* Added ZToRing lemmasGravatar jadep2017-02-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 11:56:01 +0000