partial commit: "computation" component ...

[helm.git] / matita / matita / lib / turing / multi_universal / alphabet.ma

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index fdd433f0774627924821fa1501578a45cc0ad341..1c4cd806073449a11932a251dba46b405e1fc5d5 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/alphabet.ma
+++ b/matita/matita/lib/turing/multi_universal/alphabet.ma
@@ -42,6 +42,11 @@ definition FSUnialpha ≝
   mk_FinSet DeqUnialpha [bit true;bit false;null;bar] 
   unialpha_unique unialpha_complete.
 
+unification hint  0 ≔ ; 
+    X ≟ FSUnialpha
+(* ---------------------------------------- *) ⊢ 
+    unialpha ≡ FinSetcarr X.
+    
 (*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
 definition is_bar ≝ λc:DeqUnialpha. c == bar.