aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Option.v
Commit message (Expand)AuthorAge
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
* Add option_beq_heteroGravatar Jason Gross2019-02-02
* Add some option bind lemmasGravatar Jason Gross2018-09-27
* Add some Proper lemmas for Option.bindGravatar Jason Gross2018-09-27
* Add option_beq argumentsGravatar Jason Gross2018-09-13
* Add option_beqGravatar Jason Gross2018-09-13
* Generalize option_eq to support heterogenous relationsGravatar Jason Gross2018-08-02
* Add option sequencing/returnGravatar Jason Gross2018-07-25
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
* Add Option.List.mapGravatar Jason Gross2018-06-04
* Fix a proofGravatar Jason Gross2018-04-18
* Change a proof in src/Util/OptionGravatar Jason Gross2018-04-18
* Fix a proof for Coq 8.7Gravatar Jason Gross2018-02-17
* Add lemmas about always_invert_Some and bindGravatar Jason Gross2018-02-17
* Add always_invert_SomeGravatar Jason Gross2018-02-17
* Add notation for option_bindGravatar Jason Gross2018-02-10
* Add option_map_mapGravatar Jason Gross2017-11-07
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* Work around bug in 8.4 applyGravatar Jason Gross2016-12-14
* More powerful inversion_optionGravatar Jason Gross2016-12-03
* Fix for Coq 8.5, 8.5pl1Gravatar Jason Gross2016-10-18
* generalize equiv relations in Util.Option and EdDSARepChangeGravatar Andres Erbsen2016-10-12
* Fix for Coq 8.5Gravatar Jason Gross2016-09-16
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* Make [inversion_option] work on Prop optionsGravatar Jason Gross2016-09-03
* Rename congrunce_option to inversion_option, add [inversion_prod]Gravatar Jason Gross2016-08-31
* Add congruence_option tacticGravatar Jason Gross2016-08-31
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 19:16:12 +0000