# eqdec.v -rw-r--r-- 552 bytes View raw
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Class EqDec a :=
  { eq_dec (x y: a): { x = y } + { x <> y }
  }.

Ltac decide_equality :=
  repeat match goal with
         | H: EqDec ?a |- { (_: ?a) = _ } + { _ <> _ } => apply H
         | |- { _ = _ } + { _ <> _ } => decide equality
         end.

Notation "'default_eq_dec'" := (fun _ _ => ltac:(decide_equality)).

Instance EqDec_nat: EqDec nat :=
  { eq_dec := default_eq_dec
  }.

Inductive tree a := Leaf | Node (x: a) (l r: tree a).

Instance EqDec_tree
         (a: Type) `{EqDec a}
  : EqDec (tree a). :=
  { eq_dec := default_eq_dec
  }.