From: Ferruccio Guidi Date: Wed, 6 Sep 2006 12:24:51 +0000 (+0000) Subject: plist added X-Git-Tag: 0.4.95@7852~1075 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=205276c80f0c39fe46bf2b9b7811b3343eb5c0d5;p=helm.git plist added --- diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/plist.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/plist.ma new file mode 100644 index 000000000..3a0b28571 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/plist.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/plist". + +include "ext/preamble.ma". + +inductive PList: Set \def +| PNil: PList +| PCons: nat \to (nat \to (PList \to PList)). + +definition PConsTail: + PList \to (nat \to (nat \to PList)) +\def + let rec PConsTail (hds: PList) on hds: (nat \to (nat \to PList)) \def +(\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow +(PCons h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 +h0 d0))]))) in PConsTail. + +definition Ss: + PList \to PList +\def + let rec Ss (hds: PList) on hds: PList \def (match hds with [PNil \Rightarrow +PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))]) in Ss. + diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma index bc601b309..c493641aa 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs". -include "preamble.ma". +include "../Base/theory.ma". record G : Set \def { next: (nat \to nat); diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma index 61a492535..5db781439 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs". -include "preamble.ma". +include "../Base/theory.ma". inductive B: Set \def | Abbr: B diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/preamble.ma deleted file mode 100644 index ebefd32d9..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/preamble.ma +++ /dev/null @@ -1,25 +0,0 @@ -set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/preamble". - -include "../Base/theory.ma". - -alias id "s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs/s.con". -alias id "lift_sort" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_sort.con". -alias id "lift_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_head.con". -alias id "r" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs/r.con". -alias id "r_S" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/r/props/r_S.con". -alias id "drop_gen_sort" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd/drop_gen_sort.con". -alias id "drop_gen_refl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd/drop_gen_refl.con". -alias id "drop_gen_drop" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd/drop_gen_drop.con". -alias id "drop_gen_skip_l" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd/drop_gen_skip_l.con". -alias id "r_plus_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/r/props/r_plus_sym.con". -alias id "lift_bind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_bind.con". -alias id "lift_flat" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_flat.con". -alias id "lift_d" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props/lift_d.con". -alias id "s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs/s.con". -alias id "s_plus" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/props/s_plus.con". -alias id "s_le" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/props/s_le.con". -alias id "s_plus_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/props/s_plus_sym.con". -alias id "lift_lref_lt" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_lref_lt.con". -alias id "lift_lref_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_lref_ge.con". -alias id "lift_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd/lift_head.con". -alias id "tlt_head_dx" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props/tlt_head_dx.con".