aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* make assert_preconditions way more sane; use vm_decide to kill most subgoalsGravatar jadep2017-03-02
* Separated out [carry] from other operations.Gravatar jadep2017-03-02
* Modify/add to NewBaseSystem to match with what is needed for proof of ring is...Gravatar jadep2017-03-01
* Fixed carry bugs (indexes need to be reversed, and we need to convert to/from...Gravatar jadep2017-03-01
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ...Gravatar jadep2017-03-01
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Add dlet_nd notationGravatar Jason Gross2017-03-01
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwi...Gravatar Jason Gross2017-02-28
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
* Deduplicate codeGravatar Jason Gross2017-02-28
* Defined zero and one for NewBaseSystemGravatar jadep2017-02-27
* Added operation (including creating )Gravatar jadep2017-02-27
* Added subtractionGravatar jadep2017-02-27
* added Positional wrappers for Associational operations, added correctness pro...Gravatar jadep2017-02-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:26:45 +0000