blob: 4a5872a5e0921c0ace27bc6815aa96bd2a3ea59a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
|
