--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambda_delta.info">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="applications of lambda_delta version 2"/>
+ <title>applications of lambda_delta version 2</title>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
+ <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
+ </head>
+ <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
+ <div class="head2">Contents of the Specification</div>
+ <div class="text">This specification comprises a collection of checked
+ applications of λδ version 2.
+ In particular it contains the components below.
+ </div>
+ <ul><li><span class="date">MLTT1.</span>
+ Martin-Löf's Type Theory with one universe
+ using λδ as the theory of expressions.
+ </li></ul>
+ <ul><li><span class="date">Functional.</span>
+ The validation algorithm for λδ as implemented in
+ <a href="http://lambda-delta.info/implementation.html#helena">Helena 0.8</a>.
+ </li></ul>
+
+ <div class="head2">Summary of the Specification</div>
+ <div class="text">Here is a numerical acount of the specification's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">5</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">13091</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">4</td><td class="snns plane green">lemmas</td><td class="snnn number green">1</td><td class="snns plane green">total</td><td class="ssnn number green">5</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">3</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">10</td><td class="snss plane yellow">total</td><td class="sssn number yellow">13</td></tr></tbody></table></div>
+ <ul><li><span class="date">2012 February 24.</span>
+ The Applications directory is started.
+ </li></ul>
+ <ul><li><span class="date">2011 December 20.</span>
+ The Functional component is started
+ inside the specification of λδ version 2.
+ </li></ul>
+ <ul><li><span class="date">2011 December 12.</span>
+ The MLTT1 component is started.
+ </li></ul>
+
+ <div class="head2">Logical Structure of the Specification</div>
+ <div class="text">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.
+ </div>
+ <div class="text"/>
+
+ <div class="head2">Physical Structure of the Specification</div>
+ <div class="text">The source files are grouped in directories,
+ one for each component.
+ </div>
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-03-15+01:00</div>
+</body>
+</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambda_delta.info">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="lambda_delta version 2"/>
+ <title>lambda_delta version 2</title>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
+ <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
+ </head>
+ <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
+ <div class="head2">System's Syntax and Behavior</div>
+ <div class="text">This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </div>
+ <div class="text"/>
+ <div class="text">* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </div>
+
+ <div class="head2">Summary of the Specification</div>
+ <div class="text">Here is a numerical acount of the specification's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">113</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">422759</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">45</td><td class="snns plane green">lemmas</td><td class="snnn number green">450</td><td class="snns plane green">total</td><td class="ssnn number green">495</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">31</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">39</td><td class="snss plane yellow">total</td><td class="sssn number yellow">70</td></tr></tbody></table></div>
+ <ul><li><span class="date">In progress.</span>
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </li></ul>
+ <ul><li><span class="date">In progress.</span>
+ Context-sensitive subject equivalence
+ for atomic arity assignment.
+ </li></ul>
+ <ul><li><span class="date">2012 March 15.</span>
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </li></ul>
+ <ul><li><span class="date">2012 January 27.</span>
+ Support for abstract candidates of reducibility.
+ </li></ul>
+ <ul><li><span class="date">2011 September 21.</span>
+ Confluence for context-sensitive parallel reduction.
+ </li></ul>
+ <ul><li><span class="date">2011 September 6.</span>
+ Confluence for context-free parallel reduction.
+ </li></ul>
+ <ul><li><span class="date">2011 April 17.</span>
+ Specification starts.
+ </li></ul>
+
+ <div class="head2">Logical Structure of the Specification</div>
+ <div class="text">The source files are grouped in planes and components
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
+ </div>
+ <div class="text"/>
+
+ <div class="head2">Physical Structure of the Specification</div>
+ <div class="text">The source files are grouped in directories,
+ one for each component.
+ </div>
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-03-15+01:00</div>
+</body>
+</html>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambda_delta.info">
- <head>
- <meta http-equiv="Content-Language" content="en-us"/>
- <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
- <meta http-equiv="Content-Style-Type" content="text/css"/>
- <meta name="author" content="Ferruccio Guidi"/>
- <meta name="description" content="applications of lambda_delta version 2"/>
- <title>applications of lambda_delta version 2</title>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
- <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
- </head>
- <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
- <div class="head2">Contents of the Specification</div>
- <div class="text">This specification comprises a collection of checked
- applications of λδ version 2.
- In particular it contains the components below.
- </div>
- <ul><li><span class="date">MLTT1.</span>
- Martin-Löf's Type Theory with one universe
- using λδ as the theory of expressions.
- </li></ul>
- <ul><li><span class="date">Functional.</span>
- The validation algorithm for λδ as implemented in
- <a href="http://lambda-delta.info/implementation.html#helena">Helena 0.8</a>.
- </li></ul>
-
- <div class="head2">Summary of the Specification</div>
- <div class="text">Here is a numerical acount of the specification's contents
- and its timeline.
- </div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">5</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">13091</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">4</td><td class="snns plane green">lemmas</td><td class="snnn number green">1</td><td class="snns plane green">total</td><td class="ssnn number green">5</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">3</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">10</td><td class="snss plane yellow">total</td><td class="sssn number yellow">13</td></tr></tbody></table></div>
- <ul><li><span class="date">2012 February 24.</span>
- The Applications directory is started.
- </li></ul>
- <ul><li><span class="date">2011 December 20.</span>
- The Functional component is started
- inside the specification of λδ version 2.
- </li></ul>
- <ul><li><span class="date">2011 December 12.</span>
- The MLTT1 component is started.
- </li></ul>
-
- <div class="head2">Logical Structure of the Specification</div>
- <div class="text">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.
- </div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"><br/></td><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
-
- <div class="head2">Physical Structure of the Specification</div>
- <div class="text">The source files are grouped in directories,
- one for each component.
- </div>
- <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-03-15+01:00</div>
-</body>
-</html>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambda_delta.info">
- <head>
- <meta http-equiv="Content-Language" content="en-us"/>
- <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
- <meta http-equiv="Content-Style-Type" content="text/css"/>
- <meta name="author" content="Ferruccio Guidi"/>
- <meta name="description" content="lambda_delta version 2"/>
- <title>lambda_delta version 2</title>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
- <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
- </head>
- <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
- <div class="head2">System's Syntax and Behavior</div>
- <div class="text">This is a summary of the "block structure"
- of the System's syntactic items and reductions.
- </div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns text grey">domain</td><td class="snns plane grey">block</td><td class="snns text grey">leader</td><td class="snns text grey">applicator (with →θ)*</td><td class="snns text grey">reduction</td><td class="snns text grey">→ζ *</td><td class="ssns text grey">reference *</td></tr><tr><td class="snns text">{X | Γ ⊢ X : W}</td><td class="snns plane wine">typed abstraction **</td><td class="snns text wine">Γ ⊢ λW</td><td class="snns text wine">ⓐV</td><td class="snns text wine">→β</td><td class="snns text wine">no</td><td class="ssns text wine">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane magenta">typed declaration ***</td><td class="snns text magenta">Γ ⊢ pλW</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="ssns text magenta">$p</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane prune">native type annotation *</td><td class="snns text prune">Γ ⊢ ⓣW</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="snns text prune">yes</td><td class="ssns text prune">no</td></tr><tr><td class="snns text">{X | Γ ⊢ X = V}</td><td class="snns plane blue">local abbreviation **</td><td class="snns text blue">Γ ⊢ δV</td><td class="snns text blue">no</td><td class="snns text blue">local →δ</td><td class="snns text blue">yes</td><td class="ssns text blue">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane sky">global abbreviation ***</td><td class="snns text sky">Γ ⊢ pδV</td><td class="snns text sky">no</td><td class="snns text sky">global →δ</td><td class="snns text sky">no</td><td class="ssns text sky">$p</td></tr><tr><td class="snss text">no</td><td class="snss plane cyan">sort ****</td><td class="snss text cyan">Γ ⊢ ⋆k</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="ssss text cyan">no</td></tr></tbody></table></div>
- <div class="text">* In terms only.
- ** In terms and local environments only.
- *** In global environments only.
- **** Sort level k in terms only.
- </div>
-
- <div class="head2">Summary of the Specification</div>
- <div class="text">Here is a numerical acount of the specification's contents
- and its timeline.
- </div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">113</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">422759</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">45</td><td class="snns plane green">lemmas</td><td class="snnn number green">450</td><td class="snns plane green">total</td><td class="ssnn number green">495</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">31</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">39</td><td class="snss plane yellow">total</td><td class="sssn number yellow">70</td></tr></tbody></table></div>
- <ul><li><span class="date">In progress.</span>
- Context-sensitive subject equivalence
- for native type assignment.
- </li></ul>
- <ul><li><span class="date">In progress.</span>
- Context-sensitive subject equivalence
- for atomic arity assignment.
- </li></ul>
- <ul><li><span class="date">2012 March 15.</span>
- Context-sensitive strong normalization
- for simply typed terms.
- </li></ul>
- <ul><li><span class="date">2012 January 27.</span>
- Support for abstract candidates of reducibility.
- </li></ul>
- <ul><li><span class="date">2011 September 21.</span>
- Confluence for context-sensitive parallel reduction.
- </li></ul>
- <ul><li><span class="date">2011 September 6.</span>
- Confluence for context-free parallel reduction.
- </li></ul>
- <ul><li><span class="date">2011 April 17.</span>
- Specification starts.
- </li></ul>
-
- <div class="head2">Logical Structure of the Specification</div>
- <div class="text">The source files are grouped in planes and components
- according to the following table.
- A notation file covering the whole specification is provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses.
- </div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">examples</td><td class="snns plane prune"><br/></td><td class="snns file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">native typing</td><td class="snns plane blue"><br/></td><td class="snns file blue">nty</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">equivalence</td><td class="snns plane sky">context-sensitive equivalence</td><td class="snns file sky">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file cyan">cpc_cpc</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">computation</td><td class="snns plane water">strongly normalizing computation</td><td class="snns file water">csn_vector ( ⬇* ? )</td><td class="snnn file water">csn_cpr_vector</td><td class="snnn file water">csn_tstc_vector</td><td class="snnn file water">csn_aaa</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_lift</td><td class="snnn file water">csn_cpr</td><td class="snnn file water">csn_cprs ( ⬇** ? )</td><td class="snnn file water">csn_lcpr</td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive computation</td><td class="snns file water">lcprs ( ? ⊢ ➡* ? )</td><td class="snnn file water">lcprs_cprs</td><td class="snnn file water">lcprs_lcprs</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file water">cprs_lift</td><td class="snnn file water">cprs_lcpr</td><td class="snnn file water">cprs_cprs</td><td class="snnn file water">cprs_lcprs</td><td class="snnn file water">cprs_tstc</td><td class="ssnn file water">cprs_tstc_vector</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] ⊑ ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="snnn file water">lsubc_lsuba</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )</td><td class="snnn file water">acp_aaa</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive normal forms</td><td class="snns file green">cnf ( ? ⊢ 𝐍[?] )</td><td class="snnn file green">cnf_lift</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green">lcpr_cpr</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpss</td><td class="snnn file green">cpr_ltpr</td><td class="snnn file green">cpr_cpr</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf ( 𝐖𝐇𝐍[?] )</td><td class="snnn file green">tnf ( 𝐍[?] )</td><td class="snnn file green">tnf_tif</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? ➡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green">ltpr_tps</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? ➡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="snnn file green">tpr_tpr</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf ( 𝐑[?] )</td><td class="snnn file green">tif ( 𝐈[?] )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ÷⊑ ? )</td><td class="snnn file grass">lsuba_ldrop</td><td class="snnn file grass">lsuba_aaa</td><td class="snnn file grass">lsuba_lsuba</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ÷ ? )</td><td class="snnn file grass">aaa_lift</td><td class="snnn file grass">aaa_lifts</td><td class="snnn file grass">aaa_aaa</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">term inverse relocation</td><td class="snns file yellow">delift ( ? ⊢ ? [?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss ( ? [?,?] ▶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="snnn file yellow">ltpss_ltpss</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? [?,?] ▶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow">tpss_ltps</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift</td><td class="snnn file yellow">lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @ [ ? ] ? ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="snnn file yellow">gr2_gr2</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">ltps ( ? [?,?] ▶ ? )</td><td class="snnn file orange">ltps_ldrop</td><td class="snnn file orange">ltps_tps</td><td class="snnn file orange">ltps_ltps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">tps ( ? ⊢ ? [?,?] ▶ ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] ≼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">tshf_tshf</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</td><td class="snnn file red">tstc_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @ ? )</td><td class="snnn file red">cl_weight ( #[?,?] )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #[?] )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple ( 𝐒[?] )</td><td class="snnn file red">term_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
-
- <div class="head2">Physical Structure of the Specification</div>
- <div class="text">The source files are grouped in directories,
- one for each component.
- </div>
- <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-03-15+01:00</div>
-</body>
-</html>
restarted in <a href="http://matita.cs.unibo.it/">Matita
0.5</a>.</li>
<ul>
- <li><a href="ld_apps_2.html">Here</a> is a page about
+ <li><a href="apps_2.html">Here</a> is a page about
the
topics related to the specification (Applications).</li>
- <li><a href="ld_basic_2.html">Here</a> is a page about
+ <li><a href="basic_2.html">Here</a> is a page about
the
specification (Core).<br>
</li>
height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
src="download/PNGnow2.png"><br>
<br>
- Last update 2012-0
2-24 by <a
+ Last update 2012-0
3-15 by <a
href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
Guidi</a><br>
</div>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambda_delta.info"
+ description = "applications of lambda_delta version 2"
+ title = "applications of lambda_delta version 2"
+ head = "cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)"
+>
+ <section>Contents of the Specification</section>
+ <body>This specification comprises a collection of checked
+ applications of λδ version 2.
+ In particular it contains the components below.
+ </body>
+ <news date="MLTT1.">
+ Martin-Löf's Type Theory with one universe
+ using λδ as the theory of expressions.
+ </news>
+ <news date="Functional.">
+ The validation algorithm for λδ as implemented in
+ <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+ </news>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="apps_2_sum"/>
+ <news date="2012 February 24.">
+ The Applications directory is started.
+ </news>
+ <news date="2011 December 20.">
+ The Functional component is started
+ inside the specification of λδ version 2.
+ </news>
+ <news date="2011 December 12.">
+ The MLTT1 component is started.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>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.
+ </body>
+ <table name="apps_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "ld_apps_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "MLTT1" * } {
+ [ { "" * } {
+ [ "genv_primitive" "judgement" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "functional" * } {
+ [ { "reduction and type machine" * } {
+ [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ }
+ ]
+ [ { "unfold" * } {
+ [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambda_delta.info"
+ description = "lambda_delta version 2"
+ title = "lambda_delta version 2"
+ head = "cic:/matita/lambda_delta/basic_2/ (λδ version 2)"
+>
+ <section>System's Syntax and Behavior</section>
+ <body>This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </body>
+ <table name="basic_2_blk"/>
+ <body>* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </body>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_2_sum"/>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </news>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for atomic arity assignment.
+ </news>
+ <news date="2012 March 15.">
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 January 27.">
+ Support for abstract candidates of reducibility.
+ </news>
+ <news date="2011 September 21.">
+ Confluence for context-sensitive parallel reduction.
+ </news>
+ <news date="2011 September 6.">
+ Confluence for context-free parallel reduction.
+ </news>
+ <news date="2011 April 17.">
+ Specification starts.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>The source files are grouped in planes and components
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
+ </body>
+ <table name="basic_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "ld_basic_2_blk"
+
+table {
+ class "grey" [ { "domain" * } {
+ [
+ [ "block" ] [ "leader" ]
+ [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X : W}" * } {
+ class "wine" [
+ [ "typed abstraction **" ] [ "Γ ⊢ λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
+ ]
+ class "magenta" [
+ [ "typed declaration ***" ] [ "Γ ⊢ pλW" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+ ]
+ class "prune" [
+ [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ]
+ [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X = V}" * } {
+ class "blue" [
+ [ "local abbreviation **" ] [ "Γ ⊢ δV" ]
+ [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
+ ]
+ class "sky" [
+ [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ]
+ [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
+ ]
+ } ]
+ [ { "no" * } {
+ class "cyan" [
+ [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "no" ]
+ ]
+ } ]
+}
+
+class "text" { 0 } { 2 * }
+
+class "plane" { 1 }
+
--- /dev/null
+name "ld_basic_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+ class "prune"
+ [ { "examples" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
+ ]
+ class "blue"
+ [ { "native typing" * } {
+ [ { "" * } {
+ [ "nty" * ]
+ }
+ ]
+ }
+ ]
+ class "sky"
+ [ { "equivalence" * } {
+ [ { "context-sensitive equivalence" * } {
+ [ "cpcs ( ? ⊢ ? ⬌* ? )" * ]
+ }
+ ]
+ }
+ ]
+ class "cyan"
+ [ { "conversion" * } {
+ [ { "context-sensitive conversion" * } {
+ [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
+ }
+ ]
+ }
+ ]
+ class "water"
+ [ { "computation" * } {
+ [ { "strongly normalizing computation" * } {
+ [ "csn_vector ( ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ]
+ [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ]
+ }
+ ]
+ [ { "context-sensitive computation" * } {
+ [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_cprs" "lcprs_lcprs" * ]
+ [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ]
+ }
+ ]
+ [ { "local env. ref. for abstract candidates of reducibility" * } {
+ [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
+ }
+ ]
+ [ { "support for abstract computation properties" * } {
+ [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ]
+ }
+ ]
+ }
+ ]
+ class "green"
+ [ { "reducibility" * } {
+ [ { "context-sensitive normal forms" * } {
+ [ "cnf ( ? ⊢ 𝐍[?] )" "cnf_lift" * ]
+ }
+ ]
+ [ { "context-sensitive reduction" * } {
+ [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_cpr" * ]
+ [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ]
+ }
+ ]
+ [ { "context-free normal forms" * } {
+ [ "twhnf ( 𝐖𝐇𝐍[?] )" "tnf ( 𝐍[?] )" "tnf_tif" * ]
+ }
+ ]
+ [ { "context-free reduction" * } {
+ [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" * ]
+ [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
+ }
+ ]
+ [ { "context-free reducible forms" * } {
+ [ "trf ( 𝐑[?] )" "tif ( 𝐈[?] )" * ]
+ }
+ ]
+ }
+ ]
+ class "grass"
+ [ { "static typing" * } {
+ [ { "static type assignment" * } {
+ [ "sty" "sty_lift" "sty_sty" * ]
+ }
+ ]
+ [ { "local env. ref. for atomic arity assignment" * } {
+ [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ]
+ }
+ ]
+ [ { "atomic arity assignment" * } {
+ [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ]
+ }
+ ]
+ [ { "parameters" * } {
+ [ "sh" * ]
+ }
+ ]
+ }
+ ]
+ class "yellow"
+ [ { "unfold" * } {
+ [ { "term inverse relocation" * } {
+ [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ]
+ }
+ ]
+ [ { "partial unfold" * } {
+ [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ]
+ [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
+ }
+ ]
+ [ { "generic local env. slicing" * } {
+ [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ]
+ }
+ ]
+ [ { "generic term relocation" * } {
+ [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
+ [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ]
+ }
+ ]
+ [ { "support for generic relocation" * } {
+ [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "substitution" * } {
+ [ { "parallel substitution" * } {
+ [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
+ [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
+ }
+ ]
+ [ { "global env. slicing" * } {
+ [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
+ }
+ ]
+ [ { "basic local env. slicing" * } {
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
+ }
+ ]
+ [ { "basic term relocation" * } {
+ [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
+ [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "grammar" * } {
+ [ { "local env. ref. for substitution" * } {
+ [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
+ }
+ ]
+ [ { "same head term form" * } {
+ [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
+ }
+ ]
+ [ { "same top term constructor" * } {
+ [ "tstc ( ? ≃ ? )" "tstc_tstc" "tstc_vector" * ]
+ }
+ ]
+ [ { "closures" * } {
+ [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ]
+ }
+ ]
+ [ { "internal syntax" * } {
+ [ "genv" * ]
+ [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ]
+ [ "term" "term_weight ( #[?] )" "term_simple ( 𝐒[?] )" "term_vector" * ]
+ [ "item" * ]
+ }
+ ]
+ [ { "external syntax" * } {
+ [ "aarity" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambda_delta.info"
- description = "applications of lambda_delta version 2"
- title = "applications of lambda_delta version 2"
- head = "cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)"
->
- <section>Contents of the Specification</section>
- <body>This specification comprises a collection of checked
- applications of λδ version 2.
- In particular it contains the components below.
- </body>
- <news date="MLTT1.">
- Martin-Löf's Type Theory with one universe
- using λδ as the theory of expressions.
- </news>
- <news date="Functional.">
- The validation algorithm for λδ as implemented in
- <rlink to="implementation.html#helena">Helena 0.8</rlink>.
- </news>
-
- <section>Summary of the Specification</section>
- <body>Here is a numerical acount of the specification's contents
- and its timeline.
- </body>
- <table name="ld_apps_2_sum"/>
- <news date="2012 February 24.">
- The Applications directory is started.
- </news>
- <news date="2011 December 20.">
- The Functional component is started
- inside the specification of λδ version 2.
- </news>
- <news date="2011 December 12.">
- The MLTT1 component is started.
- </news>
-
- <section>Logical Structure of the Specification</section>
- <body>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.
- </body>
- <table name="ld_apps_2_src"/>
-
- <section>Physical Structure of the Specification</section>
- <body>The source files are grouped in directories,
- one for each component.
- </body>
- <footer/>
-</page>
+++ /dev/null
-name "ld_apps_2_src"
-
-table {
- class "grey"
- [ { "component" * } {
- [ { "plane" * } {
- [ "files" * ]
- }
- ]
- }
- ]
- class "orange"
- [ { "MLTT1" * } {
- [ { "" * } {
- [ "genv_primitive" "judgement" * ]
- }
- ]
- }
- ]
- class "red"
- [ { "functional" * } {
- [ { "reduction and type machine" * } {
- [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
- }
- ]
- [ { "unfold" * } {
- [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
- }
- ]
- }
- ]
-}
-
-class "component" { 0 }
-
-class "plane" { 1 }
-
-class "file" { 2 * }
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambda_delta.info"
- description = "lambda_delta version 2"
- title = "lambda_delta version 2"
- head = "cic:/matita/lambda_delta/basic_2/ (λδ version 2)"
->
- <section>System's Syntax and Behavior</section>
- <body>This is a summary of the "block structure"
- of the System's syntactic items and reductions.
- </body>
- <table name="ld_basic_2_blk"/>
- <body>* In terms only.
- ** In terms and local environments only.
- *** In global environments only.
- **** Sort level k in terms only.
- </body>
-
- <section>Summary of the Specification</section>
- <body>Here is a numerical acount of the specification's contents
- and its timeline.
- </body>
- <table name="ld_basic_2_sum"/>
- <news date="In progress.">
- Context-sensitive subject equivalence
- for native type assignment.
- </news>
- <news date="In progress.">
- Context-sensitive subject equivalence
- for atomic arity assignment.
- </news>
- <news date="2012 March 15.">
- Context-sensitive strong normalization
- for simply typed terms.
- </news>
- <news date="2012 January 27.">
- Support for abstract candidates of reducibility.
- </news>
- <news date="2011 September 21.">
- Confluence for context-sensitive parallel reduction.
- </news>
- <news date="2011 September 6.">
- Confluence for context-free parallel reduction.
- </news>
- <news date="2011 April 17.">
- Specification starts.
- </news>
-
- <section>Logical Structure of the Specification</section>
- <body>The source files are grouped in planes and components
- according to the following table.
- A notation file covering the whole specification is provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses.
- </body>
- <table name="ld_basic_2_src"/>
-
- <section>Physical Structure of the Specification</section>
- <body>The source files are grouped in directories,
- one for each component.
- </body>
- <footer/>
-</page>
+++ /dev/null
-name "ld_basic_2_blk"
-
-table {
- class "grey" [ { "domain" * } {
- [
- [ "block" ] [ "leader" ]
- [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
- ]
- } ]
- [ { "{X | Γ ⊢ X : W}" * } {
- class "wine" [
- [ "typed abstraction **" ] [ "Γ ⊢ λW" ]
- [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
- ]
- class "magenta" [
- [ "typed declaration ***" ] [ "Γ ⊢ pλW" ]
- [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
- ]
- class "prune" [
- [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ]
- [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
- ]
- } ]
- [ { "{X | Γ ⊢ X = V}" * } {
- class "blue" [
- [ "local abbreviation **" ] [ "Γ ⊢ δV" ]
- [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
- ]
- class "sky" [
- [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ]
- [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
- ]
- } ]
- [ { "no" * } {
- class "cyan" [
- [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
- [ "no" ] [ "no" ] [ "no" ] [ "no" ]
- ]
- } ]
-}
-
-class "text" { 0 } { 2 * }
-
-class "plane" { 1 }
-
+++ /dev/null
-name "ld_basic_2_src"
-
-table {
- class "grey"
- [ { "component" * } {
- [ { "plane" * } {
- [ "files" * ]
- }
- ]
- }
- ]
- class "prune"
- [ { "examples" * } {
- [ { "" * } {
- [ "" * ]
- }
- ]
- }
- ]
- class "blue"
- [ { "native typing" * } {
- [ { "" * } {
- [ "nty" * ]
- }
- ]
- }
- ]
- class "sky"
- [ { "equivalence" * } {
- [ { "context-sensitive equivalence" * } {
- [ "cpcs ( ? ⊢ ? ⬌* ? )" * ]
- }
- ]
- }
- ]
- class "cyan"
- [ { "conversion" * } {
- [ { "context-sensitive conversion" * } {
- [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
- }
- ]
- }
- ]
- class "water"
- [ { "computation" * } {
- [ { "strongly normalizing computation" * } {
- [ "csn_vector ( ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ]
- [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ]
- }
- ]
- [ { "context-sensitive computation" * } {
- [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_cprs" "lcprs_lcprs" * ]
- [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ]
- }
- ]
- [ { "local env. ref. for abstract candidates of reducibility" * } {
- [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
- }
- ]
- [ { "support for abstract computation properties" * } {
- [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ]
- }
- ]
- }
- ]
- class "green"
- [ { "reducibility" * } {
- [ { "context-sensitive normal forms" * } {
- [ "cnf ( ? ⊢ 𝐍[?] )" "cnf_lift" * ]
- }
- ]
- [ { "context-sensitive reduction" * } {
- [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_cpr" * ]
- [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ]
- }
- ]
- [ { "context-free normal forms" * } {
- [ "twhnf ( 𝐖𝐇𝐍[?] )" "tnf ( 𝐍[?] )" "tnf_tif" * ]
- }
- ]
- [ { "context-free reduction" * } {
- [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" * ]
- [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
- }
- ]
- [ { "context-free reducible forms" * } {
- [ "trf ( 𝐑[?] )" "tif ( 𝐈[?] )" * ]
- }
- ]
- }
- ]
- class "grass"
- [ { "static typing" * } {
- [ { "static type assignment" * } {
- [ "sty" "sty_lift" "sty_sty" * ]
- }
- ]
- [ { "local env. ref. for atomic arity assignment" * } {
- [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ]
- }
- ]
- [ { "atomic arity assignment" * } {
- [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ]
- }
- ]
- [ { "parameters" * } {
- [ "sh" * ]
- }
- ]
- }
- ]
- class "yellow"
- [ { "unfold" * } {
- [ { "term inverse relocation" * } {
- [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ]
- }
- ]
- [ { "partial unfold" * } {
- [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ]
- [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
- }
- ]
- [ { "generic local env. slicing" * } {
- [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ]
- }
- ]
- [ { "generic term relocation" * } {
- [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
- [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ]
- }
- ]
- [ { "support for generic relocation" * } {
- [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
- }
- ]
- }
- ]
- class "orange"
- [ { "substitution" * } {
- [ { "parallel substitution" * } {
- [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
- [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
- }
- ]
- [ { "global env. slicing" * } {
- [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
- }
- ]
- [ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
- }
- ]
- [ { "basic term relocation" * } {
- [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
- [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
- }
- ]
- }
- ]
- class "red"
- [ { "grammar" * } {
- [ { "local env. ref. for substitution" * } {
- [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
- }
- ]
- [ { "same head term form" * } {
- [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
- }
- ]
- [ { "same top term constructor" * } {
- [ "tstc ( ? ≃ ? )" "tstc_tstc" "tstc_vector" * ]
- }
- ]
- [ { "closures" * } {
- [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ]
- }
- ]
- [ { "internal syntax" * } {
- [ "genv" * ]
- [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ]
- [ "term" "term_weight ( #[?] )" "term_simple ( 𝐒[?] )" "term_vector" * ]
- [ "item" * ]
- }
- ]
- [ { "external syntax" * } {
- [ "aarity" * ]
- }
- ]
- }
- ]
-}
-
-class "component" { 0 }
-
-class "plane" { 1 }
-
-class "file" { 2 * }
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<!-- This file was generated by xhtbl.native, do not edit -->
-
-<xsl:stylesheet version="1.0"
- xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns="http://www.w3.org/1999/xhtml"
->
-
-<xsl:template name="ld_basic_2_blk">
- <table cellpadding="4" cellspacing="0">
- <tbody>
- <tr>
- <td class="snns text grey">domain</td>
- <td class="snns plane grey">block</td>
- <td class="snns text grey">leader</td>
- <td class="snns text grey">applicator (with →θ)*</td>
- <td class="snns text grey">reduction</td>
- <td class="snns text grey">→ζ *</td>
- <td class="ssns text grey">reference *</td>
- </tr>
- <tr>
- <td class="snns text">{X | Γ ⊢ X : W}</td>
- <td class="snns plane wine">typed abstraction **</td>
- <td class="snns text wine">Γ ⊢ λW</td>
- <td class="snns text wine">ⓐV</td>
- <td class="snns text wine">→β</td>
- <td class="snns text wine">no</td>
- <td class="ssns text wine">#i</td>
- </tr>
- <tr>
- <td class="nnns text"><br/></td>
- <td class="snns plane magenta">typed declaration ***</td>
- <td class="snns text magenta">Γ ⊢ pλW</td>
- <td class="snns text magenta">no</td>
- <td class="snns text magenta">no</td>
- <td class="snns text magenta">no</td>
- <td class="ssns text magenta">$p</td>
- </tr>
- <tr>
- <td class="nnns text"><br/></td>
- <td class="snns plane prune">native type annotation *</td>
- <td class="snns text prune">Γ ⊢ ⓣW</td>
- <td class="snns text prune">no</td>
- <td class="snns text prune">no</td>
- <td class="snns text prune">yes</td>
- <td class="ssns text prune">no</td>
- </tr>
- <tr>
- <td class="snns text">{X | Γ ⊢ X = V}</td>
- <td class="snns plane blue">local abbreviation **</td>
- <td class="snns text blue">Γ ⊢ δV</td>
- <td class="snns text blue">no</td>
- <td class="snns text blue">local →δ</td>
- <td class="snns text blue">yes</td>
- <td class="ssns text blue">#i</td>
- </tr>
- <tr>
- <td class="nnns text"><br/></td>
- <td class="snns plane sky">global abbreviation ***</td>
- <td class="snns text sky">Γ ⊢ pδV</td>
- <td class="snns text sky">no</td>
- <td class="snns text sky">global →δ</td>
- <td class="snns text sky">no</td>
- <td class="ssns text sky">$p</td>
- </tr>
- <tr>
- <td class="snss text">no</td>
- <td class="snss plane cyan">sort ****</td>
- <td class="snss text cyan">Γ ⊢ ⋆k</td>
- <td class="snss text cyan">no</td>
- <td class="snss text cyan">no</td>
- <td class="snss text cyan">no</td>
- <td class="ssss text cyan">no</td>
- </tr>
- </tbody>
- </table>
-</xsl:template>
-
-</xsl:stylesheet>
projects / helm.git / commitdiff