(****** DeqSet: a set with a decidbale equality ******)
-record DeqSet : Type[1] ≝ { carr :> Type[0];
+record DeqSet : Type[1] ≝ {
+ carr :> Type[0];
eqb: carr → carr → bool;
eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
}.
-
+
notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
interpretation "eqb" 'eqb a b = (eqb ? a b).
(* ---------------------------------------- *) ⊢
eq_option T a1 a2 ≡ eqb X a1 a2.
+
(* pairs *)
definition eq_pairs ≝
λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
-
+
+(*
unification hint 0 ≔ C,P;
T ≟ carr C,
X ≟ DeqSig C P
X ≟ DeqSig T P
(* ---------------------------------------- *) ⊢
eq_sigma T P p1 p2 ≡ eqb X p1 p2.
-
+*)