aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Decidable.v
Commit message (Expand)AuthorAge
* Fix opacity of dec_Forall, dec_ExistsGravatar Jason Gross2017-11-10
* Add dec_if_boolGravatar Jason Gross2017-11-10
* Add dec_Forall, dec_ExistsGravatar Jason Gross2017-11-09
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Add dec_eq_comparisonGravatar Jason Gross2017-06-13
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Revert "Add dec_eq_positive"Gravatar Jason Gross2017-05-16
* Add dec_eq_positiveGravatar Jason Gross2017-05-16
* Add dec_of_bool_decGravatar Jason Gross2017-04-10
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Add dec_eq_positiveGravatar Jason Gross2017-03-17
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Decidable: add [Z] and [nat] inequalitiesGravatar Andres Erbsen2016-10-10
* Add dec eq for option, listGravatar Jason Gross2016-09-18
* Add a lemma about semidecidable things to DecidableGravatar Jason Gross2016-09-05
* address code review commentsGravatar Andres Erbsen2016-08-04
* prove eqsig_eq using hprop in Decidable.vGravatar Andres Erbsen2016-08-04
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Add a commentGravatar Jason Gross2016-08-01
* Better transparency of dec_eq_sig_hpropGravatar Jason Gross2016-08-01
* Add instances to decide equality of sigma typesGravatar Jason Gross2016-07-29
* Add decidable instances for sumwise and fieldwiseGravatar Jason Gross2016-06-27
* Use Decidable machinery for is_eq_decGravatar Jason Gross2016-06-24
* Fix for broken abstractGravatar Jason Gross2016-06-22
* Add decidability util fileGravatar Jason Gross2016-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 18:31:05 +0000