michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Regenerated files after bug-fix in agda2html.

Browse source
This commit is contained in:
Pepijn Kokke 2017-03-11 23:53:35 +00:00
parent 7d5f1f0bb2
commit d5a9a6345a
No known key found for this signature in database
GPG key ID: EF467CD387487CB8
5 changed files with 3135 additions and 3137 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
out/Basics.md
View file

@ -23,13 +23,13 @@ permalink : /Basics
> </a
><a name="169" class="Symbol"
>(</a
><a name="170" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="170" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>_&#8801;_</a
><a name="173" class="Symbol"
>;</a
><a name="174"
> </a
><a name="175" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="175" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="179" class="Symbol"
>)</a
@ -394,7 +394,7 @@ form of an Agda type:
>)</a
><a name="4150"
> </a
><a name="4151" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="4151" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="4152"
> </a
@ -419,7 +419,7 @@ a term of the above type:
>=</a
><a name="4490"
> </a
><a name="4491" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="4491" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>

102
out/Maps.md
View file

@ -76,19 +76,19 @@ standard library, wherever they overlap.
> </a
><a name="1526" class="Symbol"
>(</a
><a name="1527" href="Agda.Builtin.Bool.html#67" class="Datatype"
><a name="1527" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#67" class="Datatype"
>Bool</a
><a name="1531" class="Symbol"
>;</a
><a name="1532"
> </a
><a name="1533" href="Agda.Builtin.Bool.html#92" class="InductiveConstructor"
><a name="1533" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#92" class="InductiveConstructor"
>true</a
><a name="1537" class="Symbol"
>;</a
><a name="1538"
> </a
><a name="1539" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="1539" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="1544" class="Symbol"
>)</a
@ -181,7 +181,7 @@ standard library, wherever they overlap.
> </a
><a name="1686" class="Symbol"
>(</a
><a name="1687" href="Agda.Builtin.Nat.html#97" class="Datatype"
><a name="1687" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#97" class="Datatype"
>&#8469;</a
><a name="1688" class="Symbol"
>)</a
@ -279,7 +279,7 @@ function for ids and its fundamental property.
>:</a
><a name="2264"
> </a
><a name="2265" href="Agda.Builtin.Nat.html#97" class="Datatype"
><a name="2265" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#97" class="Datatype"
>&#8469;</a
><a name="2266"
> </a
@ -335,7 +335,7 @@ function for ids and its fundamental property.
>x</a
><a name="2322"
> </a
><a name="2323" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="2323" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="2324"
> </a
@ -431,7 +431,7 @@ function for ids and its fundamental property.
>yes</a
><a name="2399"
> </a
><a name="2400" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="2400" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="2404"
>
@ -522,7 +522,7 @@ function for ids and its fundamental property.
>x</a
><a name="2482"
> </a
><a name="2483" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="2483" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="2484"
> </a
@ -542,7 +542,7 @@ function for ids and its fundamental property.
>x</a
><a name="2493"
> </a
><a name="2494" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="2494" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="2495"
> </a
@ -555,7 +555,7 @@ function for ids and its fundamental property.
>id-inj</a
><a name="2508"
> </a
><a name="2509" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="2509" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="2513"
> </a
@ -563,7 +563,7 @@ function for ids and its fundamental property.
>=</a
><a name="2515"
> </a
><a name="2516" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="2516" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -888,7 +888,7 @@ like this:
>TotalMap</a
><a name="4527"
> </a
><a name="4528" href="Agda.Builtin.Bool.html#67" class="Datatype"
><a name="4528" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#67" class="Datatype"
>Bool</a
><a name="4532"
>
@ -917,7 +917,7 @@ like this:
>empty</a
><a name="4569"
> </a
><a name="4570" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="4570" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="4575" class="Symbol"
>)</a
@ -935,7 +935,7 @@ like this:
>)</a
><a name="4583"
> </a
><a name="4584" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="4584" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="4589" class="Symbol"
>)</a
@ -953,7 +953,7 @@ like this:
>)</a
><a name="4597"
> </a
><a name="4598" href="Agda.Builtin.Bool.html#92" class="InductiveConstructor"
><a name="4598" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#92" class="InductiveConstructor"
>true</a
>
{% endraw %}</pre>
@ -987,11 +987,11 @@ application!
>)</a
><a name="4807"
> </a
><a name="4808" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="4808" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="4809"
> </a
><a name="4810" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="4810" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="4815"
>
@ -1004,7 +1004,7 @@ application!
>=</a
><a name="4836"
> </a
><a name="4837" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="4837" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="4841"
>
@ -1034,11 +1034,11 @@ application!
>)</a
><a name="4881"
> </a
><a name="4882" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="4882" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="4883"
> </a
><a name="4884" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="4884" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="4889"
>
@ -1051,7 +1051,7 @@ application!
>=</a
><a name="4910"
> </a
><a name="4911" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="4911" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="4915"
>
@ -1081,11 +1081,11 @@ application!
>)</a
><a name="4955"
> </a
><a name="4956" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="4956" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="4957"
> </a
><a name="4958" href="Agda.Builtin.Bool.html#86" class="InductiveConstructor"
><a name="4958" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#86" class="InductiveConstructor"
>false</a
><a name="4963"
>
@ -1098,7 +1098,7 @@ application!
>=</a
><a name="4984"
> </a
><a name="4985" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="4985" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="4989"
>
@ -1128,11 +1128,11 @@ application!
>)</a
><a name="5029"
> </a
><a name="5030" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="5030" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="5031"
> </a
><a name="5032" href="Agda.Builtin.Bool.html#92" class="InductiveConstructor"
><a name="5032" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Bool.html#92" class="InductiveConstructor"
>true</a
><a name="5036"
>
@ -1145,7 +1145,7 @@ application!
>=</a
><a name="5057"
> </a
><a name="5058" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="5058" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -1194,7 +1194,7 @@ First, the empty map returns its default element for all keys:
>x</a
><a name="5612"
> </a
><a name="5613" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="5613" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="5614"
> </a
@ -1233,7 +1233,7 @@ First, the empty map returns its default element for all keys:
>x</a
><a name="5705"
> </a
><a name="5706" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="5706" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="5707"
> </a
@ -1250,7 +1250,7 @@ First, the empty map returns its default element for all keys:
>=</a
><a name="5726"
> </a
><a name="5727" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="5727" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -1344,7 +1344,7 @@ back $$v$$:
>x</a
><a name="6055"
> </a
><a name="6056" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="6056" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="6057"
> </a
@ -1432,7 +1432,7 @@ back $$v$$:
>x</a
><a name="6186"
> </a
><a name="6187" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="6187" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="6188"
> </a
@ -1490,7 +1490,7 @@ back $$v$$:
>=</a
><a name="6236"
> </a
><a name="6237" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="6237" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="6241"
>
@ -1525,7 +1525,7 @@ back $$v$$:
>x&#8800;x</a
><a name="6271"
> </a
><a name="6272" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="6272" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="6276" class="Symbol"
>)</a
@ -1636,7 +1636,7 @@ the same result that $$m$$ would have given:
>y</a
><a name="6621"
> </a
><a name="6622" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="6622" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="6623"
> </a
@ -1743,7 +1743,7 @@ the same result that $$m$$ would have given:
>=</a
><a name="6714"
> </a
><a name="6715" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="6715" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -1858,7 +1858,7 @@ the second `update` on $$m$$:
>y</a
><a name="7212"
> </a
><a name="7213" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="7213" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="7214"
> </a
@ -1986,7 +1986,7 @@ the second `update` on $$m$$:
>y</a
><a name="7388"
> </a
><a name="7389" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="7389" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="7390"
> </a
@ -2069,7 +2069,7 @@ the second `update` on $$m$$:
>=</a
><a name="7466"
> </a
><a name="7467" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="7467" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="7471"
>
@ -2214,7 +2214,7 @@ result is equal to $$m$$:
>y</a
><a name="7847"
> </a
><a name="7848" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="7848" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="7849"
> </a
@ -2316,7 +2316,7 @@ result is equal to $$m$$:
>y</a
><a name="7988"
> </a
><a name="7989" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="7989" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="7990"
> </a
@ -2391,7 +2391,7 @@ result is equal to $$m$$:
>=</a
><a name="8060"
> </a
><a name="8061" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="8061" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="8065"
>
@ -2416,7 +2416,7 @@ result is equal to $$m$$:
>=</a
><a name="8083"
> </a
><a name="8084" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="8084" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -2551,7 +2551,7 @@ updates.
><a name="8466"
>
</a
><a name="8496" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="8496" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="8497"
> </a
@ -2716,7 +2716,7 @@ updates.
><a name="8705"
>
</a
><a name="8734" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="8734" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="8735"
> </a
@ -3409,7 +3409,7 @@ partial maps.
>x</a
><a name="9876"
> </a
><a name="9877" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="9877" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="9878"
> </a
@ -3549,7 +3549,7 @@ partial maps.
>y</a
><a name="10044"
> </a
><a name="10045" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="10045" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="10046"
> </a
@ -3705,7 +3705,7 @@ partial maps.
>y</a
><a name="10240"
> </a
><a name="10241" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="10241" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="10242"
> </a
@ -3837,7 +3837,7 @@ partial maps.
>x</a
><a name="10412"
> </a
><a name="10413" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="10413" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="10414"
> </a
@ -3878,7 +3878,7 @@ partial maps.
>y</a
><a name="10454"
> </a
><a name="10455" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="10455" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="10456"
> </a
@ -4063,7 +4063,7 @@ partial maps.
><a name="10684"
>
</a
><a name="10712" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="10712" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="10713"
> </a

46
out/Stlc.md
View file

@ -145,25 +145,25 @@ permalink : /Stlc
> </a
><a name="322" class="Symbol"
>(</a
><a name="323" href="Agda.Builtin.Nat.html#97" class="Datatype"
><a name="323" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#97" class="Datatype"
>&#8469;</a
><a name="324" class="Symbol"
>;</a
><a name="325"
> </a
><a name="326" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor"
><a name="326" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#128" class="InductiveConstructor"
>suc</a
><a name="329" class="Symbol"
>;</a
><a name="330"
> </a
><a name="331" href="Agda.Builtin.Nat.html#115" class="InductiveConstructor"
><a name="331" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#115" class="InductiveConstructor"
>zero</a
><a name="335" class="Symbol"
>;</a
><a name="336"
> </a
><a name="337" href="Agda.Builtin.Nat.html#230" class="Primitive Operator"
><a name="337" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#230" class="Primitive Operator"
>_+_</a
><a name="340" class="Symbol"
>)</a
@ -293,7 +293,7 @@ permalink : /Stlc
> </a
><a name="529" class="Symbol"
>(</a
><a name="530" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="530" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>_&#8801;_</a
><a name="533" class="Symbol"
>;</a
@ -305,7 +305,7 @@ permalink : /Stlc
>;</a
><a name="539"
> </a
><a name="540" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="540" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="544" class="Symbol"
>)</a
@ -791,7 +791,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
>id</a
><a name="6245"
> </a
><a name="6246" href="Agda.Builtin.Nat.html#115" class="InductiveConstructor"
><a name="6246" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#115" class="InductiveConstructor"
>zero</a
><a name="6250"
> = </a
@ -816,11 +816,11 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
>id</a
><a name="6273"
> (</a
><a name="6275" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor"
><a name="6275" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#128" class="InductiveConstructor"
>suc</a
><a name="6278"
> </a
><a name="6279" href="Agda.Builtin.Nat.html#115" class="InductiveConstructor"
><a name="6279" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#115" class="InductiveConstructor"
>zero</a
><a name="6283"
>) = </a
@ -845,15 +845,15 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
>id</a
><a name="6307"
> (</a
><a name="6309" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor"
><a name="6309" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#128" class="InductiveConstructor"
>suc</a
><a name="6312"
> (</a
><a name="6314" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor"
><a name="6314" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#128" class="InductiveConstructor"
>suc</a
><a name="6317"
> </a
><a name="6318" href="Agda.Builtin.Nat.html#115" class="InductiveConstructor"
><a name="6318" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#115" class="InductiveConstructor"
>zero</a
><a name="6322"
>)) = </a
@ -1409,7 +1409,7 @@ Agda makes the first choice---for example,
>:</a
><a name="8605"
> </a
><a name="8606" href="Agda.Builtin.Nat.html#97" class="Datatype"
><a name="8606" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#97" class="Datatype"
>&#8469;</a
><a name="8607" class="Symbol"
>)</a
@ -1423,7 +1423,7 @@ Agda makes the first choice---for example,
>3</a
><a name="8612"
> </a
><a name="8613" href="Agda.Builtin.Nat.html#230" class="Primitive Operator"
><a name="8613" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#230" class="Primitive Operator"
>+</a
><a name="8614"
> </a
@ -1433,7 +1433,7 @@ Agda makes the first choice---for example,
>)</a
><a name="8617"
> </a
><a name="8618" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="8618" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="8619"
> </a
@ -1451,7 +1451,7 @@ Agda makes the first choice---for example,
>:</a
><a name="8627"
> </a
><a name="8628" href="Agda.Builtin.Nat.html#97" class="Datatype"
><a name="8628" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#97" class="Datatype"
>&#8469;</a
><a name="8629" class="Symbol"
>)</a
@ -1476,7 +1476,7 @@ Agda makes the first choice---for example,
>=</a
><a name="8663"
> </a
><a name="8664" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="8664" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
@ -2501,7 +2501,7 @@ above.
>t</a
><a name="13734"
> </a
><a name="13735" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="13735" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="13736"
> </a
@ -4035,7 +4035,7 @@ $$\Gamma$$."
>x</a
><a name="19152"
> </a
><a name="19153" href="Agda.Builtin.Equality.html#83" class="Datatype Operator"
><a name="19153" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#83" class="Datatype Operator"
>&#8801;</a
><a name="19154"
> </a
@ -4563,7 +4563,7 @@ $$\Gamma$$."
>x</a
><a name="19909"
> </a
><a name="19910" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="19910" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="19914" class="Symbol"
>)</a
@ -4764,7 +4764,7 @@ $$\varnothing\vdash \lambda x:A. \lambda y:A\rightarrow A. y\;(y\;x) : A\rightar
>y</a
><a name="20275"
> </a
><a name="20276" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="20276" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="20280" class="Symbol"
>)</a
@ -4787,7 +4787,7 @@ $$\varnothing\vdash \lambda x:A. \lambda y:A\rightarrow A. y\;(y\;x) : A\rightar
>y</a
><a name="20301"
> </a
><a name="20302" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="20302" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="20306" class="Symbol"
>)</a
@ -4803,7 +4803,7 @@ $$\varnothing\vdash \lambda x:A. \lambda y:A\rightarrow A. y\;(y\;x) : A\rightar
>x</a
><a name="20314"
> </a
><a name="20315" href="Agda.Builtin.Equality.html#140" class="InductiveConstructor"
><a name="20315" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
><a name="20319" class="Symbol"
>)</a

6029
out/StlcProp.md
View file

File diff suppressed because it is too large Load diff

87
src/StlcProp.lagda
View file

@ -19,17 +19,17 @@ open import Stlc
</div>
In this chapter, we develop the fundamental theory of the Simply
Typed Lambda Calculus -- in particular, the type safety
Typed Lambda Calculus---in particular, the type safety
theorem.
## Canonical Forms
As we saw for the simple calculus in the [Stlc](Stlc.html) chapter, the
first step in establishing basic properties of reduction and types
is to identify the possible _canonical forms_ (i.e., well-typed
closed values) belonging to each type. For $$bool$$, these are the boolean
values $$true$$ and $$false$$. For arrow types, the canonical forms
are lambda-abstractions.
As we saw for the simple calculus in the [Stlc]({{ "Stlc" | relative_url }})
chapter, the first step in establishing basic properties of reduction and types
is to identify the possible _canonical forms_ (i.e., well-typed closed values)
belonging to each type. For $$bool$$, these are the boolean values $$true$$ and
$$false$$. For arrow types, the canonical forms are lambda-abstractions.
\begin{code}
CanonicalForms : Term → Type → Set
@ -48,8 +48,8 @@ As before, the _progress_ theorem tells us that closed, well-typed
terms are not stuck: either a well-typed term is a value, or it
can take a reduction step. The proof is a relatively
straightforward extension of the progress proof we saw in the
[Stlc](Stlc.html) chapter. We'll give the proof in English first,
then the formal version.
[Stlc]({{ "Stlc" | relative_url }}) chapter. We'll give the proof in English
first, then the formal version.
\begin{code}
progress : ∀ {t A} → ∅ ⊢ t ∶ A → Value t ⊎ ∃ λ t′ → t ==> t′
@ -136,11 +136,11 @@ technical lemmas that are needed by various cases of the more
interesting proofs), the story goes like this:
- The _preservation theorem_ is proved by induction on a typing
derivation, pretty much as we did in the [Stlc](Stlc.html)
chapter. The one case that is significantly different is the
one for the $$red$$ rule, whose definition uses the substitution
operation. To see that this step preserves typing, we need to
know that the substitution itself does. So we prove a...
derivation, pretty much as we did in the [Stlc]({{ "Stlc" | relative_url }})
chapter. The one case that is significantly different is the one for the
$$red$$ rule, whose definition uses the substitution operation. To see that
this step preserves typing, we need to know that the substitution itself
does. So we prove a...
- _substitution lemma_, stating that substituting a (closed)
term $$s$$ for a variable $$x$$ in a term $$t$$ preserves the type
@ -154,12 +154,12 @@ interesting proofs), the story goes like this:
we prove a...
- _context invariance_ lemma, showing that typing is preserved
under "inessential changes" to the context $$\Gamma$$ -- in
under "inessential changes" to the context $$\Gamma$$---in
particular, changes that do not affect any of the free
variables of the term. And finally, for this, we need a
careful definition of...
- the _free variables_ of a term -- i.e., those variables
- the _free variables_ of a term---i.e., those variables
mentioned in a term and not in the scope of an enclosing
function abstraction binding a variable of the same name.
@ -332,7 +332,7 @@ $$\Gamma \vdash t \in T$$.
$$\Gamma', y:A$$.
- If the last rule was `app`, then $$t = t_1\;t_2$$, with
$$\Gamma \vdash t_1 : A\to T$$ and $$\Gamma \vdash t_2 : A$$.
$$\Gamma \vdash t_1:A\to T$$ and $$\Gamma \vdash t_2:A$$.
One induction hypothesis states that for all contexts $$\Gamma'$$,
if $$\Gamma'$$ agrees with $$\Gamma$$ on the free variables in $$t_1$$,
then $$t_1$$ has type $$A\to T$$ under $$\Gamma'$$; there is a similar IH
@ -364,7 +364,7 @@ replaceCtxt f (if t₁∶bool then t₂∶A else t₃∶A)
\end{code}
Now we come to the conceptual heart of the proof that reduction
preserves types -- namely, the observation that _substitution_
preserves types---namely, the observation that _substitution_
preserves types.
Formally, the so-called _Substitution Lemma_ says this: Suppose we
@ -387,12 +387,12 @@ $$\Gamma \vdash [x:=v]t : T$$.
\end{code}
One technical subtlety in the statement of the lemma is that
we assign $$v$$ the type $$U$$ in the _empty_ context -- in other
we assign $$v$$ the type $$U$$ in the _empty_ context---in other
words, we assume $$v$$ is closed. This assumption considerably
simplifies the $$abs$$ case of the proof (compared to assuming
$$\Gamma \vdash v : U$$, which would be the other reasonable assumption
at this point) because the context invariance lemma then tells us
that $$v$$ has type $$U$$ in any context at all -- we don't have to
that $$v$$ has type $$U$$ in any context at all---we don't have to
worry about free variables in $$v$$ clashing with the variable being
introduced into the context by $$abs$$.
@ -401,7 +401,7 @@ property. Intuitively, it says that substitution and typing can
be done in either order: we can either assign types to the terms
$$t$$ and $$v$$ separately (under suitable contexts) and then combine
them using substitution, or we can substitute first and then
assign a type to $$ $$x:=v$$ t $$ -- the result is the same either
assign a type to $$ $$x:=v$$ t $$---the result is the same either
way.
_Proof_: We show, by induction on $$t$$, that for all $$T$$ and
@ -412,7 +412,7 @@ $$\Gamma$$, if $$\Gamma,x:U \vdash t : T$$ and $$\vdash v : U$$, then $$\Gamma
depending on whether $$t$$ is $$x$$ or some other variable.
- If $$t = x$$, then from the fact that $$\Gamma, x:U \vdash x :
T$$ we conclude that $$U = T$$. We must show that $$$$x:=v$$x =
T$$ we conclude that $$U = T$$. We must show that $$[x:=v]x =
v$$ has type $$T$$ under $$\Gamma$$, given the assumption that
$$v$$ has type $$U = T$$ under the empty context. This
follows from context invariance: if a closed term has type
@ -422,9 +422,9 @@ $$\Gamma$$, if $$\Gamma,x:U \vdash t : T$$ and $$\vdash v : U$$, then $$\Gamma
we need only note that $$y$$ has the same type under $$\Gamma,
x:U$$ as under $$\Gamma$$.
- If $$t$$ is an abstraction $$\lambda y:T_11. t_12$$, then the IH tells us,
for all $$\Gamma'$$ and $$T'$$, that if $$\Gamma',x:U \vdash t_12 : T'$$
and $$\vdash v : U$$, then $$\Gamma' \vdash $$x:=v$$t_12 : T'$$.
- If $$t$$ is an abstraction $$\lambda y:t_{11}. t_{12}$$, then the IH tells us,
for all $$\Gamma'$$ and $$T'$$, that if $$\Gamma',x:U \vdash t_{12}:T'$$
and $$\vdash v:U$$, then $$\Gamma' \vdash [x:=v]t_{12}:T'$$.
The substitution in the conclusion behaves differently
depending on whether $$x$$ and $$y$$ are the same variable.
@ -432,17 +432,17 @@ $$\Gamma$$, if $$\Gamma,x:U \vdash t : T$$ and $$\vdash v : U$$, then $$\Gamma
First, suppose $$x = y$$. Then, by the definition of
substitution, $$[x:=v]t = t$$, so we just need to show $$\Gamma \vdash
t : T$$. But we know $$\Gamma,x:U \vdash t : T$$, and, since $$y$$
does not appear free in $$\lambda y:T_11. t_12$$, the context invariance
does not appear free in $$\lambda y:t_{11}. t_{12}$$, the context invariance
lemma yields $$\Gamma \vdash t : T$$.
Second, suppose $$x <> y$$. We know $$\Gamma,x:U,y:T_11 \vdash t_12 :
T_12$$ by inversion of the typing relation, from which
$$\Gamma,y:T_11,x:U \vdash t_12 : T_12$$ follows by the context
invariance lemma, so the IH applies, giving us $$\Gamma,y:T_11 \vdash
$$x:=v$$t_12 : T_12$$. By $$abs$$, $$\Gamma \vdash \lambda y:T_11. $$x:=v$$t_12
: T_11→T_12$$, and by the definition of substitution (noting
that $$x <> y$$), $$\Gamma \vdash \lambda y:T_11. $$x:=v$$t_12 : T_11→T_12$$ as
required.
Second, suppose $$x \neq y$$. We know $$\Gamma,x:U,y:t_{11} \vdash
t_{12}:t_{12}$$ by inversion of the typing relation, from which
$$\Gamma,y:t_{11},x:U \vdash t_{12}:t_{12}$$ follows by the context invariance
lemma, so the IH applies, giving us $$\Gamma,y:t_{11} \vdash
[x:=v]t_{12}:t_{12}$$. By $$abs$$, $$\Gamma \vdash \lambda y:t_{11}.
[x:=v]t_{12}:t_{11}\to t_{12}$$, and by the definition of substitution (noting
that $$x \neq y$$), $$\Gamma \vdash \lambda y:t_{11}. [x:=v]t_{12}:t_{11}\to
t_{12}$$ as required.
- If $$t$$ is an application $$t_1 t_2$$, the result follows
straightforwardly from the definition of substitution and the
@ -454,8 +454,8 @@ One more technical note: This proof is a rare case where an
induction on terms, rather than typing derivations, yields a
simpler argument. The reason for this is that the assumption
$$update Gamma x U \vdash t : T$$ is not completely generic, in the
sense that one of the "slots" in the typing relation -- namely the
context -- is not just a variable, and this means that Agda's
sense that one of the "slots" in the typing relation---namely the
context---is not just a variable, and this means that Agda's
native induction tactic does not give us the induction hypothesis
that we want. It is possible to work around this, but the needed
generalization is a little tricky. The term $$t$$, on the other
@ -506,7 +506,7 @@ _Proof_: By induction on the derivation of $$\vdash t : T$$.
- The $$Sapp2$$ case is similar.
- If $$t_1 t_2$$ takes a step by $$Sred$$, then $$t_1 =
\lambda x:T_11.t_12$$ and $$t_1 t_2$$ steps to $$$$x:=t_2$$t_12$$; the
\lambda x:t_{11}.t_{12}$$ and $$t_1 t_2$$ steps to $$$$x:=t_2$$t_{12}$$; the
desired result now follows from the fact that substitution
preserves types.
@ -531,17 +531,16 @@ Proof with eauto.
(* Most of the cases are immediate by induction,
and $$eauto$$ takes care of them
+ (* Sred
apply substitution_preserves_typing with T_11...
apply substitution_preserves_typing with t_{11}...
inversion HT_1...
Qed.
#### Exercise: 2 stars, recommended (subject_expansion_stlc)
An exercise in the $$Stlc$$$$sf/Stlc.html$$ chapter asked about the subject
expansion property for the simple language of arithmetic and
boolean expressions. Does this property hold for STLC? That is,
is it always the case that, if $$t ==> t'$$ and $$has_type t' T$$,
then $$empty \vdash t : T$$? If so, prove it. If not, give a
counter-example not involving conditionals.
An exercise in the [Stlc]({{ "Stlc" | relative_url }}) chapter asked about the
subject expansion property for the simple language of arithmetic and boolean
expressions. Does this property hold for STLC? That is, is it always the case
that, if $$t ==> t'$$ and $$has_type t' T$$, then $$empty \vdash t : T$$? If
so, prove it. If not, give a counter-example not involving conditionals.
(* FILL IN HERE