aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* changed names of ops in NewBaseSystem to reflect that they are sig and not sigTGravatar jadep2017-02-27
* Modified lemma and created tactic to handle it; added reduce step to multipl...Gravatar jadep2017-02-26
* removed leftover saturated stuff (will probably end up in a separate file som...Gravatar jadep2017-02-26
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Add log and non-log versions of FixedWordSizes lemGravatar Jason Gross2017-02-23
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* Minor change to reflection namingGravatar Jason Gross2017-02-23
* added explanation of why CPS is usefulGravatar jadep2017-02-23
* Removed code that will be completely replaced in the future; replaced some po...Gravatar jadep2017-02-22
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* moved more stuff to NUtilGravatar jadep2017-02-22
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* categorize the rest of the stuff in Ed25519Gravatar jadep2017-02-22
* categorize some of the stuff in Ed25519Gravatar jadep2017-02-22
* NewBaseSystem: less verboseGravatar Andres Erbsen2017-02-22
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 12:19:46 +0000