From: Ferruccio Guidi Date: Tue, 28 Oct 2014 17:04:59 +0000 (+0000) Subject: \lambda\delta version 2A released on Web site X-Git-Tag: make_still_working~807 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e258362c37ec6d9132ec57bd5e4987d148c10799;p=helm.git \lambda\delta version 2A released on Web site --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index e4499a294..dada75abd 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -1,11 +1,13 @@ -
Contents of the Specification
+ + + Contents of the Specification This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below. @@ -21,7 +23,7 @@ Helena 0.8. -
Summary of the Specification
+ Summary of the Specification Here is a numerical acount of the specification's contents and its timeline. @@ -37,12 +39,8 @@ The MLTT1 component is started. -
Logical Structure of the Specification
- The source files are grouped in planes and components - according to the following table. - Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + Logical Structure of the Specification + This table reports the specification's components and their planes. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index f69061eaf..6b5037b85 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -1,10 +1,11 @@ + -
Summary of the Specification
+ Summary of the Specification Here is a numerical acount of the specification's contents and its timeline.
- Stage "B" + Stage "B" Context-sensitive subject equivalence for native type assignment. - Stage "A": "Weakening the Applicability Condition" + Stage "A": "Extending the Applicability Condition" + + λδ version 2A is released. + Iterated static type assignment defined (more elegantly) as a primitive notion. @@ -100,12 +104,8 @@ Specification starts. -
Logical Structure of the Specification
- The source files are grouped in planes and components - according to the following table. - Notation files covering the whole specification are provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + Logical Structure of the Specification + This table reports the specification's components and their planes.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml index 522ac9312..9c79f972c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -1,17 +1,15 @@ -
Summary of the Specification
+ + + Summary of the Specification Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].
@@ -21,12 +19,8 @@ Specification starts. -
Logical Structure of the Specification
- The source files are grouped in planes - according to the following table. - Notation files covering the whole specification are provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + Logical Structure of the Specification + This table reports the specification's components and their planes.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 6d8d7435c..9f478280f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -2,30 +2,47 @@ name "ground_2_src" table { class "gray" - [ { "plane" * } { - [ "files" * ] + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] } ] class "yellow" [ { "natural numbers with infinity" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" - "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" - "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" - "ynat_max" "ynat_min" * ] + [ { "" * } { + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" + "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" + "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" + "ynat_max" "ynat_min" * + ] + } + ] } ] class "orange" [ { "extensions to the library" * } { - [ "arith.ma ( ?^? )" * ] + [ { "" * } { + [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? )" + "list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * + ] + } + ] } ] class "red" [ { "generated logical decomposables" * } { - [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ] + [ { "" * } { + [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ] + } + ] } ] } -class "top" { * } +class "top" { * } -class "italic" { 0 } +class "capitalize italic" { 0 } + +class "italic" { 1 }