blob: 5118ddb4724745b343b44ede17543e366549c25a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}.
Proof.
pose (diseq := false).
decide equality.
Defined.
Set Mangle Names.
Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}.
Proof.
decide equality. (*Error: Anomaly "variable diseq unbound." ...*)
Defined.
|
