From 14aa468ded0030440dbc9cc8fb5b936d927bb6fd Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 17 Mar 2010 11:48:50 +0000 Subject: [PATCH 1/1] Aggiornamento alla negazione. --- helm/software/matita/nlibrary/basics/list.ma | 2 +- helm/software/matita/nlibrary/basics/list2.ma | 30 +++++++++++++++++++ 2 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/nlibrary/basics/list2.ma diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma index 92eddc705..d30ed7dfc 100644 --- a/helm/software/matita/nlibrary/basics/list.ma +++ b/helm/software/matita/nlibrary/basics/list.ma @@ -39,7 +39,7 @@ ndefinition not_nil: ∀A:Type.list A → Prop ≝ ntheorem nil_cons: ∀A:Type.∀l:list A.∀a:A. a::l ≠ []. - #A; #l; #a; #Heq; nchange with (not_nil ? (a::l)); + #A; #l; #a; napply nmk; #Heq; nchange with (not_nil ? (a::l)); nrewrite > Heq; //; nqed. diff --git a/helm/software/matita/nlibrary/basics/list2.ma b/helm/software/matita/nlibrary/basics/list2.ma new file mode 100644 index 000000000..1dd62c114 --- /dev/null +++ b/helm/software/matita/nlibrary/basics/list2.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/list.ma". +include "arithmetics/nat.ma". + +nlet rec length (A:Type) (l:list A) on l ≝ + match l with + [ nil ⇒ 0 + | cons a tl ⇒ S (length A tl)]. + +notation "|M|" non associative with precedence 60 for @{'norm $M}. +interpretation "norm" 'norm l = (length ? l). + +nlet rec nth n (A:Type) (l:list A) (d:A) ≝ + match n with + [O ⇒ hd A l d + |S m ⇒ nth m A (tail A l) d]. + -- 2.39.2