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 (file)
index 0000000..3a0b285
--- /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 bc601b30942b4b1343b6010186b80d0da2ecd47a..c493641aaceaf41b663a21ecebc35b7a9d3c1cf2 100644 (file)
--- 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 61a492535a7cc78bf1d9ab49f02f30dd14fdd28f..5db7814395963a8d6ed448877342094142e967ea 100644 (file)
--- 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 (file)
index ebefd32..0000000
--- 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".