From 77ad7d412890919298a21903dd4884359cc4f6cd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 29 Sep 2005 14:56:55 +0000 Subject: [PATCH] moved a (commented) test in a handier position --- helm/matita/library/list/list.ma | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma index 1973dadab..72637c357 100644 --- a/helm/matita/library/list/list.ma +++ b/helm/matita/library/list/list.ma @@ -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 <> []. -- 2.39.2