diff options
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. |