]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/first.ma
merged cic_notation with matita: good luck!
[helm.git] / helm / matita / tests / first.ma
index d75f372cea9d75bd4a8cccf3f99b14b8771305eb..69b4adf26f4221a6a19b006617740fe4e253c0b4 100644 (file)
@@ -10,7 +10,6 @@ inductive eq (A:Set): A \to A \to Prop \def
 inductive list (A:Set) : Set \def
   | nil : list A
   | cons : A \to list A \to list A.
-alias symbol "cast" (instance 0) = "type cast".
 
 let rec list_len (A:Set) (l:list A) on l \def
   [\lambda x.nat]