]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/list/list.ma
moved a (commented) test in a handier position
[helm.git] / helm / matita / library / list / list.ma
index 1973dadab299683c4d775d2d409cdc764843faf4..72637c357226ae4c0c51304d4b73b246958b61aa 100644 (file)
@@ -36,6 +36,8 @@ interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
 interpretation "cons" 'cons hd tl =
   (cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
 
+(* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
+
 theorem nil_cons:
   \forall A:Set.\forall l:list A.\forall a:A.
     a::l <> [].