From: Ferruccio Guidi Date: Wed, 21 Oct 2015 16:50:43 +0000 (+0000) Subject: minor update X-Git-Tag: make_still_working~682 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=361a91ade954f92013da892c62d41e3a7168cfc0;p=helm.git minor update --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt index 0ff386374..68140c8e8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt @@ -125,10 +125,7 @@ leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 lift1/fwd lift1_cons_tail -lift1/fwd lifts1_nil -lift1/fwd lifts1_cons lift/props lifts_tapp -lift/props lifts_inj llt/props lweight_repl llt/props llt_repl llt/props llt_trans 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 93b218306..fd37f2b13 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 @@ -32,8 +32,14 @@ Stage "A": "Extending the Applicability Condition" + + λδ version 2A2 is started. + + + λδ version 2A1 appears too complex and is dismissed. + - λδ version 2A is released. + λδ version 2A1 is released. Iterated static type assignment defined (more elegantly) @@ -101,7 +107,7 @@ Confluence for context-free parallel reduction on terms. - Specification starts. + λδ version 2 is started. Logical Structure of the Specification