1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "datatypes/bool.ma".
16 include "sets/setoids.ma".
20 [ true ⇒ match b with [ true ⇒ True | _ ⇒ False ]
21 | false ⇒ match b with [ false ⇒ True | _ ⇒ False ]].
23 (* XXX move to bool *)
24 interpretation "bool eq" 'eq_low a b = (eq_bool a b).
26 ndefinition BOOL : setoid.
27 @bool; @(eq_bool); #x; ncases x; //; #y; ncases y; //; #z; ncases z; //; nqed.
29 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
30 alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)".
31 unification hint 0 ≔ ;
32 P1 ≟ refl ? (eq0 BOOL),
33 P2 ≟ sym ? (eq0 BOOL),
34 P3 ≟ trans ? (eq0 BOOL),
35 X ≟ mk_setoid bool (mk_equivalence_relation ? (eq_bool) P1 P2 P3)
36 (*-----------------------------------------------------------------------*) ⊢
39 unification hint 0 ≔ a,b;
42 (* -------------------------------------------- *) ⊢
43 eq_bool a b ≡ eq_rel L R a b.