Progress

[helm.git] / matita / matita / lib / basics / deqsets.ma

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index 2d6434f6578ffc2f4440aa5843388068be8e22ba..45afabe59ad9555e55f863c8b9e3a584c5ac5963 100644 (file)
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -28,6 +28,10 @@ notation "\P H" non associative with precedence 90
 notation "\b H" non associative with precedence 90 
   for @{(proj2 … (eqb_true ???) $H)}. 
   
+notation < "𝐃" non associative with precedence 90 
+ for @{'bigD}.
+interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
+  
 lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
   (eqb ? a b) = false ↔ a ≠ b.
 #S #a #b % #H 
@@ -57,6 +61,7 @@ qed.
 
 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint  0 ≔ ; 
     X ≟ mk_DeqSet bool beqb beqb_true
 (* ---------------------------------------- *) ⊢