]> matita.cs.unibo.it Git - helm.git/commitdiff
moved a (commented) test in a handier position
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Sep 2005 14:56:55 +0000 (14:56 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Sep 2005 14:56:55 +0000 (14:56 +0000)
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 <> [].