Skip to content

Commit f5cd195

Browse files
ppedrotppedrot
committed
Version the documentation
1 parent 1e1af19 commit f5cd195

File tree

64 files changed

+40582
-916
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

64 files changed

+40582
-916
lines changed

‎docs/coqdoc/.gitignore‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎docs/coqdoc/LogRel.AutoSubst.Ast.html‎

Lines changed: 1491 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/coqdoc/LogRel.AutoSubst.Extra.html‎

Lines changed: 163 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/coqdoc/LogRel.AutoSubst.core.html‎

Lines changed: 205 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/coqdoc/LogRel.AutoSubst.unscoped.html‎

Lines changed: 381 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/coqdoc/LogRel.BasicAst.html‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
2+
<html xmlns="http://www.w3.org/1999/xhtml">
3+
4+
<head>
5+
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
6+
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
7+
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
8+
<script type="text/javascript" src="config.js"></script>
9+
<script type="text/javascript" src="coqdocjs.js"></script>
10+
</head>
11+
12+
<body onload="document.getElementById('content').focus()">
13+
<div id="header">
14+
<span class="left">
15+
<span class="modulename"> <script> document.write(document.title) </script> </span>
16+
</span>
17+
18+
<span class="button" id="toggle-proofs"></span>
19+
20+
<span class="right">
21+
<a href="../">Project Page</a>
22+
<a href="./indexpage.html"> Index </a>
23+
<a href="./toc.html"> Table of Contents </a>
24+
</span>
25+
</div>
26+
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
27+
<div id="main">
28+
<h1 class="libtitle">LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations…</h1>
29+
30+
<div class="code">
31+
</div>
32+
33+
<div class="doc">
34+
35+
</div>
36+
<div class="code">
37+
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Strings.String.html#"><span class="id" title="library">String</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Bool.Bool.html#"><span class="id" title="library">Bool</span></a>.<br/>
38+
<span class="id" title="keyword">From</span> <span class="id" title="var">LogRel.AutoSubst</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="LogRel.AutoSubst.core.html#"><span class="id" title="library">core</span></a> <a class="idref" href="LogRel.AutoSubst.unscoped.html#"><span class="id" title="library">unscoped</span></a>.<br/>
39+
40+
<br/>
41+
<span class="id" title="keyword">Inductive</span> <a id="sort" class="idref" href="#sort"><span class="id" title="definition, inductive"><span id="sort_rect" class="id"><span id="sort_ind" class="id"><span id="sort_rec" class="id"><span id="sort_sind" class="id">sort</span></span></span></span></span></a> : <span class="id" title="keyword">Set</span> :=<br/>
42+
&nbsp;&nbsp;| <a id="set" class="idref" href="#set"><span class="id" title="constructor">set</span></a> : <a class="idref" href="LogRel.BasicAst.html#sort:1"><span class="id" title="inductive">sort</span></a>.<br/>
43+
44+
<br/>
45+
<span class="id" title="keyword">Definition</span> <a id="sort_of_product" class="idref" href="#sort_of_product"><span class="id" title="definition">sort_of_product</span></a> (<a id="s:3" class="idref" href="#s:3"><span class="id" title="binder">s</span></a> <a id="s':4" class="idref" href="#s':4"><span class="id" title="binder">s'</span></a> : <a class="idref" href="LogRel.BasicAst.html#sort"><span class="id" title="inductive">sort</span></a>) := <a class="idref" href="LogRel.BasicAst.html#set"><span class="id" title="constructor">set</span></a>.<br/>
46+
</div>
47+
</div>
48+
<div id="footer">
49+
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
50+
</div>
51+
</div>
52+
</body>
53+
54+
</html>

‎docs/coqdoc/LogRel.Context.html‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
2+
<html xmlns="http://www.w3.org/1999/xhtml">
3+
4+
<head>
5+
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
6+
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
7+
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
8+
<script type="text/javascript" src="config.js"></script>
9+
<script type="text/javascript" src="coqdocjs.js"></script>
10+
</head>
11+
12+
<body onload="document.getElementById('content').focus()">
13+
<div id="header">
14+
<span class="left">
15+
<span class="modulename"> <script> document.write(document.title) </script> </span>
16+
</span>
17+
18+
<span class="button" id="toggle-proofs"></span>
19+
20+
<span class="right">
21+
<a href="../">Project Page</a>
22+
<a href="./indexpage.html"> Index </a>
23+
<a href="./toc.html"> Table of Contents </a>
24+
</span>
25+
</div>
26+
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
27+
<div id="main">
28+
<h1 class="libtitle">LogRel.Context: definition of contexts and operations on them.</h1>
29+
30+
<div class="code">
31+
</div>
32+
33+
<div class="doc">
34+
35+
</div>
36+
<div class="code">
37+
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.ssr.ssreflect.html#"><span class="id" title="library">ssreflect</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Classes.Morphisms.html#"><span class="id" title="library">Morphisms</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Setoids.Setoid.html#"><span class="id" title="library">Setoid</span></a>.<br/>
38+
<span class="id" title="keyword">From</span> <span class="id" title="var">LogRel.AutoSubst</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="LogRel.AutoSubst.core.html#"><span class="id" title="library">core</span></a> <a class="idref" href="LogRel.AutoSubst.unscoped.html#"><span class="id" title="library">unscoped</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#"><span class="id" title="library">Ast</span></a> <a class="idref" href="LogRel.AutoSubst.Extra.html#"><span class="id" title="library">Extra</span></a>.<br/>
39+
<span class="id" title="keyword">From</span> <span class="id" title="var">LogRel</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="LogRel.Utils.html#"><span class="id" title="library">Utils</span></a> <a class="idref" href="LogRel.BasicAst.html#"><span class="id" title="library">BasicAst</span></a>.<br/>
40+
41+
<br/>
42+
<span class="id" title="keyword">Set</span> <span class="id" title="var">Primitive</span> <span class="id" title="var">Projections</span>.<br/>
43+
44+
<br/>
45+
</div>
46+
47+
<div class="doc">
48+
<a id="lab18"></a><h2 class="section">Context declaration</h2>
49+
Context: list of declarations Terms use de Bruijn indices to refer to context entries.
50+
</div>
51+
<div class="code">
52+
53+
<br/>
54+
<span class="id" title="keyword">Definition</span> <a id="context" class="idref" href="#context"><span class="id" title="definition">context</span></a> := <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#Core.term"><span class="id" title="inductive">term</span></a>.<br/>
55+
56+
<br/>
57+
<span class="id" title="keyword">Notation</span> <a id="bfa9fae25f9bf698daae93f61b5313af" class="idref" href="#bfa9fae25f9bf698daae93f61b5313af"><span class="id" title="notation">&quot;</span></a>'ε'" := (@<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#Core.term"><span class="id" title="inductive">term</span></a>).<br/>
58+
<span class="id" title="keyword">Notation</span> <a id="b66601545ff7e22c5dcb7c86aa0cca21" class="idref" href="#b66601545ff7e22c5dcb7c86aa0cca21"><span class="id" title="notation">&quot;</span></a> Γ ,, d " := (@<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#Core.term"><span class="id" title="inductive">term</span></a> <span class="id" title="var">d</span> <span class="id" title="var">Γ</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 20, <span class="id" title="var">d</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>).<br/>
59+
<span class="id" title="keyword">Notation</span> <a id="9c82c702508313fd669cee3f1f4704ce" class="idref" href="#9c82c702508313fd669cee3f1f4704ce"><span class="id" title="notation">&quot;</span></a> Γ ,,, Δ " := (@<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#app"><span class="id" title="definition">app</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#Core.term"><span class="id" title="inductive">term</span></a> <span class="id" title="var">Δ</span> <span class="id" title="var">Γ</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 25, <span class="id" title="var">Δ</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
60+
61+
<br/>
62+
</div>
63+
64+
<div class="doc">
65+
States that a definition, correctly weakened, is in a context.
66+
</div>
67+
<div class="code">
68+
<span class="id" title="keyword">Inductive</span> <a id="in_ctx" class="idref" href="#in_ctx"><span class="id" title="definition, inductive"><span id="in_ctx_rect" class="id"><span id="in_ctx_ind" class="id"><span id="in_ctx_rec" class="id"><span id="in_ctx_sind" class="id">in_ctx</span></span></span></span></span></a> : <a class="idref" href="LogRel.Context.html#context"><span class="id" title="definition">context</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="LogRel.AutoSubst.Ast.html#Core.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Type</span> :=<br/>
69+
&nbsp;&nbsp;| <a id="in_here" class="idref" href="#in_here"><span class="id" title="constructor">in_here</span></a> (<a id="55485d85e29df2faa6748490a2d4cd13" class="idref" href="#55485d85e29df2faa6748490a2d4cd13"><span class="id" title="binder">Γ</span></a> : <a class="idref" href="LogRel.Context.html#context"><span class="id" title="definition">context</span></a>) <a id="d:4" class="idref" href="#d:4"><span class="id" title="binder">d</span></a> : <a class="idref" href="LogRel.Context.html#in_ctx:1"><span class="id" title="inductive">in_ctx</span></a> (<a class="idref" href="LogRel.Context.html#55485d85e29df2faa6748490a2d4cd13"><span class="id" title="variable">Γ</span></a><a class="idref" href="LogRel.Context.html#b66601545ff7e22c5dcb7c86aa0cca21"><span class="id" title="notation">,,</span></a><a class="idref" href="LogRel.Context.html#d:4"><span class="id" title="variable">d</span></a>) 0 (<a class="idref" href="LogRel.Context.html#d:4"><span class="id" title="variable">d</span></a><a class="idref" href="LogRel.AutoSubst.Extra.html#6b0dc8bbfc65c6aaca075257dfbbe0c7"><span class="id" title="notation">⟨</span></a><a class="idref" href="LogRel.AutoSubst.Extra.html#a71e0ec29d2f17f624c1b8cb2190d19b"><span class="id" title="notation">↑</span></a><a class="idref" href="LogRel.AutoSubst.Extra.html#6b0dc8bbfc65c6aaca075257dfbbe0c7"><span class="id" title="notation">⟩</span></a>)<br/>
70+
&nbsp;&nbsp;| <a id="in_there" class="idref" href="#in_there"><span class="id" title="constructor">in_there</span></a> (<a id="a66eb0e7c85ea280f33904e5ac83af54" class="idref" href="#a66eb0e7c85ea280f33904e5ac83af54"><span class="id" title="binder">Γ</span></a> : <a class="idref" href="LogRel.Context.html#context"><span class="id" title="definition">context</span></a>) <a id="d:6" class="idref" href="#d:6"><span class="id" title="binder">d</span></a> <a id="d':7" class="idref" href="#d':7"><span class="id" title="binder">d'</span></a> <a id="n:8" class="idref" href="#n:8"><span class="id" title="binder">n</span></a> : <a class="idref" href="LogRel.Context.html#in_ctx:1"><span class="id" title="inductive">in_ctx</span></a> <a class="idref" href="LogRel.Context.html#a66eb0e7c85ea280f33904e5ac83af54"><span class="id" title="variable">Γ</span></a> <a class="idref" href="LogRel.Context.html#n:8"><span class="id" title="variable">n</span></a> <a class="idref" href="LogRel.Context.html#d:6"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="LogRel.Context.html#in_ctx:1"><span class="id" title="inductive">in_ctx</span></a> (<a class="idref" href="LogRel.Context.html#a66eb0e7c85ea280f33904e5ac83af54"><span class="id" title="variable">Γ</span></a><a class="idref" href="LogRel.Context.html#b66601545ff7e22c5dcb7c86aa0cca21"><span class="id" title="notation">,,</span></a><a class="idref" href="LogRel.Context.html#d':7"><span class="id" title="variable">d'</span></a>) (<a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="LogRel.Context.html#n:8"><span class="id" title="variable">n</span></a>) (<a class="idref" href="LogRel.AutoSubst.Ast.html#Core.ren_term"><span class="id" title="definition">ren_term</span></a> <a class="idref" href="LogRel.AutoSubst.unscoped.html#shift"><span class="id" title="definition">shift</span></a> <a class="idref" href="LogRel.Context.html#d:6"><span class="id" title="variable">d</span></a>).<br/>
71+
72+
<br/>
73+
<span class="id" title="keyword">Lemma</span> <a id="in_ctx_inj" class="idref" href="#in_ctx_inj"><span class="id" title="lemma">in_ctx_inj</span></a> <a id="a27a3f5be2c643b658176c4fa6dd32d6" class="idref" href="#a27a3f5be2c643b658176c4fa6dd32d6"><span class="id" title="binder">Γ</span></a> <a id="n:10" class="idref" href="#n:10"><span class="id" title="binder">n</span></a> <a id="decl:11" class="idref" href="#decl:11"><span class="id" title="binder">decl</span></a> <a id="decl':12" class="idref" href="#decl':12"><span class="id" title="binder">decl'</span></a> :<br/>
74+
&nbsp;&nbsp;<a class="idref" href="LogRel.Context.html#in_ctx"><span class="id" title="inductive">in_ctx</span></a> <a class="idref" href="LogRel.Context.html#a27a3f5be2c643b658176c4fa6dd32d6"><span class="id" title="variable">Γ</span></a> <a class="idref" href="LogRel.Context.html#n:10"><span class="id" title="variable">n</span></a> <a class="idref" href="LogRel.Context.html#decl:11"><span class="id" title="variable">decl</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="LogRel.Context.html#in_ctx"><span class="id" title="inductive">in_ctx</span></a> <a class="idref" href="LogRel.Context.html#a27a3f5be2c643b658176c4fa6dd32d6"><span class="id" title="variable">Γ</span></a> <a class="idref" href="LogRel.Context.html#n:10"><span class="id" title="variable">n</span></a> <a class="idref" href="LogRel.Context.html#decl':12"><span class="id" title="variable">decl'</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="LogRel.Context.html#decl:11"><span class="id" title="variable">decl</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.19.2/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="LogRel.Context.html#decl':12"><span class="id" title="variable">decl'</span></a>.<br/>
75+
<span class="id" title="keyword">Proof</span>.<br/>
76+
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> 1 <span class="id" title="tactic">in</span> <span class="id" title="var">decl'</span> |- * ; <span class="id" title="tactic">inversion</span> 1 ; <span class="id" title="tactic">subst</span>.<br/>
77+
&nbsp;&nbsp;1: <span class="id" title="tactic">reflexivity</span>.<br/>
78+
&nbsp;&nbsp;<span class="id" title="var">now</span> <span class="id" title="tactic">f_equal</span>.<br/>
79+
<span class="id" title="keyword">Qed</span>.<br/>
80+
</div>
81+
</div>
82+
<div id="footer">
83+
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
84+
</div>
85+
</div>
86+
</body>
87+
88+
</html>

0 commit comments

Comments
 (0)