diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-23 21:59:09 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-23 21:59:09 -0400 |
commit | c9f4cf296671baf01f3f08d2e027b415ef014059 (patch) | |
tree | cdd4d413c4bd60c571db0167b9c7050b5e618968 /src/Util/MSetPositive | |
parent | 4ad320a862e34e6a831e0f05c148c6abb54889d4 (diff) |
Add some equality lemmas about Positive{Map,Set}
Diffstat (limited to 'src/Util/MSetPositive')
-rw-r--r-- | src/Util/MSetPositive/Equality.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Util/MSetPositive/Equality.v b/src/Util/MSetPositive/Equality.v new file mode 100644 index 000000000..4a5872a5e --- /dev/null +++ b/src/Util/MSetPositive/Equality.v @@ -0,0 +1,15 @@ +Require Import Coq.MSets.MSetPositive. +Require Import Crypto.Util.Bool.Equality. +Require Import Crypto.Util.Decidable. + +Module PositiveSet. + Scheme Equality for PositiveSet.tree. + + Notation t_beq := tree_beq. + Notation t_eq_dec := tree_eq_dec. + Notation internal_t_dec_bl := internal_tree_dec_bl. + Notation internal_t_dec_lb := internal_tree_dec_lb. + + Global Instance tree_dec_eq : DecidableRel (@eq PositiveSet.tree) := tree_eq_dec. + Global Instance t_dec_eq : DecidableRel (@eq PositiveSet.t) := t_eq_dec. +End PositiveSet. |