Re-generated files after removing --strip-implicits
This commit is contained in:
Pepijn Kokke
parent
d1163c6f39
commit
c11978a133
3 changed files with 3994 additions and 3021 deletions
6224
out/Maps.md
6224
out/Maps.md
File diff suppressed because it is too large
Load diff
345
out/Stlc.md
345
out/Stlc.md
|
|
@ -24,25 +24,25 @@ permalink : /Stlc
|
||||||
> </a
|
> </a
|
||||||
><a name="157" class="Symbol"
|
><a name="157" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="158" href="Maps.html#2243" class="Datatype"
|
><a name="158" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="160" class="Symbol"
|
><a name="160" class="Symbol"
|
||||||
>;</a
|
>;</a
|
||||||
><a name="161"
|
><a name="161"
|
||||||
> </a
|
> </a
|
||||||
><a name="162" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="162" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="164" class="Symbol"
|
><a name="164" class="Symbol"
|
||||||
>;</a
|
>;</a
|
||||||
><a name="165"
|
><a name="165"
|
||||||
> </a
|
> </a
|
||||||
><a name="166" href="Maps.html#2297" class="Function Operator"
|
><a name="166" href="Maps.html#2344" class="Function Operator"
|
||||||
>_≟_</a
|
>_≟_</a
|
||||||
><a name="169" class="Symbol"
|
><a name="169" class="Symbol"
|
||||||
>;</a
|
>;</a
|
||||||
><a name="170"
|
><a name="170"
|
||||||
> </a
|
> </a
|
||||||
><a name="171" href="Maps.html#9362" class="Function"
|
><a name="171" href="Maps.html#9409" class="Function"
|
||||||
>PartialMap</a
|
>PartialMap</a
|
||||||
><a name="181" class="Symbol"
|
><a name="181" class="Symbol"
|
||||||
>;</a
|
>;</a
|
||||||
|
|
@ -52,7 +52,7 @@ permalink : /Stlc
|
||||||
>module</a
|
>module</a
|
||||||
><a name="189"
|
><a name="189"
|
||||||
> </a
|
> </a
|
||||||
><a name="190" href="Maps.html#9451" class="Module"
|
><a name="190" href="Maps.html#9498" class="Module"
|
||||||
>PartialMap</a
|
>PartialMap</a
|
||||||
><a name="200" class="Symbol"
|
><a name="200" class="Symbol"
|
||||||
>)</a
|
>)</a
|
||||||
|
|
@ -83,7 +83,7 @@ permalink : /Stlc
|
||||||
>;</a
|
>;</a
|
||||||
><a name="234"
|
><a name="234"
|
||||||
> </a
|
> </a
|
||||||
><a name="235" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
|
><a name="235" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function"
|
||||||
>⊥-elim</a
|
>⊥-elim</a
|
||||||
><a name="241" class="Symbol"
|
><a name="241" class="Symbol"
|
||||||
>)</a
|
>)</a
|
||||||
|
|
@ -559,7 +559,7 @@ so we will STLC's function type as `_⇒_`.
|
||||||
>:</a
|
>:</a
|
||||||
><a name="5528"
|
><a name="5528"
|
||||||
> </a
|
> </a
|
||||||
><a name="5529" href="Maps.html#2243" class="Datatype"
|
><a name="5529" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="5531"
|
><a name="5531"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -609,7 +609,7 @@ so we will STLC's function type as `_⇒_`.
|
||||||
>:</a
|
>:</a
|
||||||
><a name="5577"
|
><a name="5577"
|
||||||
> </a
|
> </a
|
||||||
><a name="5578" href="Maps.html#2243" class="Datatype"
|
><a name="5578" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="5580"
|
><a name="5580"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -735,7 +735,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>=</a
|
>=</a
|
||||||
><a name="6206"
|
><a name="6206"
|
||||||
> </a
|
> </a
|
||||||
><a name="6207" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6207" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6209"
|
><a name="6209"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -752,7 +752,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>=</a
|
>=</a
|
||||||
><a name="6215"
|
><a name="6215"
|
||||||
> </a
|
> </a
|
||||||
><a name="6216" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6216" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6218"
|
><a name="6218"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -769,7 +769,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>=</a
|
>=</a
|
||||||
><a name="6224"
|
><a name="6224"
|
||||||
> </a
|
> </a
|
||||||
><a name="6225" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6225" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6227"
|
><a name="6227"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -787,7 +787,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>DISPLAY</a
|
>DISPLAY</a
|
||||||
><a name="6242"
|
><a name="6242"
|
||||||
> </a
|
> </a
|
||||||
><a name="6243" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6243" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6245"
|
><a name="6245"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -812,7 +812,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>DISPLAY</a
|
>DISPLAY</a
|
||||||
><a name="6270"
|
><a name="6270"
|
||||||
> </a
|
> </a
|
||||||
><a name="6271" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6271" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6273"
|
><a name="6273"
|
||||||
> (</a
|
> (</a
|
||||||
|
|
@ -841,7 +841,7 @@ that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
|
||||||
>DISPLAY</a
|
>DISPLAY</a
|
||||||
><a name="6304"
|
><a name="6304"
|
||||||
> </a
|
> </a
|
||||||
><a name="6305" href="Maps.html#2260" class="InductiveConstructor"
|
><a name="6305" href="Maps.html#2307" class="InductiveConstructor"
|
||||||
>id</a
|
>id</a
|
||||||
><a name="6307"
|
><a name="6307"
|
||||||
> (</a
|
> (</a
|
||||||
|
|
@ -1528,6 +1528,23 @@ second choice here.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="8945"
|
><a name="8945"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="8946" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="8947" href="Stlc.html#8947" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="8948"
|
||||||
|
> </a
|
||||||
|
><a name="8949" href="Stlc.html#8949" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="8950"
|
||||||
|
> </a
|
||||||
|
><a name="8951" href="Stlc.html#8951" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="8952" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="8953"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="8962" class="Symbol"
|
><a name="8962" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="8963"
|
><a name="8963"
|
||||||
|
|
@ -1689,7 +1706,7 @@ $$
|
||||||
>:</a
|
>:</a
|
||||||
><a name="12138"
|
><a name="12138"
|
||||||
> </a
|
> </a
|
||||||
><a name="12139" href="Maps.html#2243" class="Datatype"
|
><a name="12139" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="12141"
|
><a name="12141"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -1758,7 +1775,7 @@ $$
|
||||||
>x</a
|
>x</a
|
||||||
><a name="12191"
|
><a name="12191"
|
||||||
> </a
|
> </a
|
||||||
><a name="12192" href="Maps.html#2297" class="Function Operator"
|
><a name="12192" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="12193"
|
><a name="12193"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -1970,7 +1987,7 @@ $$
|
||||||
>x</a
|
>x</a
|
||||||
><a name="12322"
|
><a name="12322"
|
||||||
> </a
|
> </a
|
||||||
><a name="12323" href="Maps.html#2297" class="Function Operator"
|
><a name="12323" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="12324"
|
><a name="12324"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -2333,7 +2350,7 @@ above.
|
||||||
>:</a
|
>:</a
|
||||||
><a name="13541"
|
><a name="13541"
|
||||||
> </a
|
> </a
|
||||||
><a name="13542" href="Maps.html#2243" class="Datatype"
|
><a name="13542" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="13544" class="Symbol"
|
><a name="13544" class="Symbol"
|
||||||
>)</a
|
>)</a
|
||||||
|
|
@ -2635,6 +2652,27 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15090"
|
><a name="15090"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15091" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15092" href="Stlc.html#15092" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="15093"
|
||||||
|
> </a
|
||||||
|
><a name="15094" href="Stlc.html#15094" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="15095"
|
||||||
|
> </a
|
||||||
|
><a name="15096" href="Stlc.html#15096" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15097"
|
||||||
|
> </a
|
||||||
|
><a name="15098" href="Stlc.html#15098" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15099" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15100"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15111" class="Symbol"
|
><a name="15111" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15112"
|
><a name="15112"
|
||||||
|
|
@ -2721,6 +2759,23 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15181"
|
><a name="15181"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15182" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15183" href="Stlc.html#15183" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15184"
|
||||||
|
> </a
|
||||||
|
><a name="15185" href="Stlc.html#15185" class="Bound"
|
||||||
|
>s'</a
|
||||||
|
><a name="15187"
|
||||||
|
> </a
|
||||||
|
><a name="15188" href="Stlc.html#15188" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15189" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15190"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15201" class="Symbol"
|
><a name="15201" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15202"
|
><a name="15202"
|
||||||
|
|
@ -2783,6 +2838,23 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15258"
|
><a name="15258"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15259" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15260" href="Stlc.html#15260" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15261"
|
||||||
|
> </a
|
||||||
|
><a name="15262" href="Stlc.html#15262" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15263"
|
||||||
|
> </a
|
||||||
|
><a name="15264" href="Stlc.html#15264" class="Bound"
|
||||||
|
>t'</a
|
||||||
|
><a name="15266" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15267"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15278" class="Symbol"
|
><a name="15278" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15279"
|
><a name="15279"
|
||||||
|
|
@ -2858,6 +2930,27 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15355"
|
><a name="15355"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15356" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15357" href="Stlc.html#15357" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15358"
|
||||||
|
> </a
|
||||||
|
><a name="15359" href="Stlc.html#15359" class="Bound"
|
||||||
|
>s'</a
|
||||||
|
><a name="15361"
|
||||||
|
> </a
|
||||||
|
><a name="15362" href="Stlc.html#15362" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15363"
|
||||||
|
> </a
|
||||||
|
><a name="15364" href="Stlc.html#15364" class="Bound"
|
||||||
|
>u</a
|
||||||
|
><a name="15365" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15366"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15377" class="Symbol"
|
><a name="15377" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15378"
|
><a name="15378"
|
||||||
|
|
@ -2944,6 +3037,19 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15456"
|
><a name="15456"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15457" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15458" href="Stlc.html#15458" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15459"
|
||||||
|
> </a
|
||||||
|
><a name="15460" href="Stlc.html#15460" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15461" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15462"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15473" class="Symbol"
|
><a name="15473" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15474"
|
><a name="15474"
|
||||||
|
|
@ -2993,6 +3099,19 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15516"
|
><a name="15516"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15517" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15518" href="Stlc.html#15518" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="15519"
|
||||||
|
> </a
|
||||||
|
><a name="15520" href="Stlc.html#15520" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15521" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15522"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15533" class="Symbol"
|
><a name="15533" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15534"
|
><a name="15534"
|
||||||
|
|
@ -3128,6 +3247,14 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15727"
|
><a name="15727"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15728" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15729" href="Stlc.html#15729" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="15730" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15731"
|
||||||
|
> </a
|
||||||
><a name="15732" class="Symbol"
|
><a name="15732" class="Symbol"
|
||||||
>-></a
|
>-></a
|
||||||
><a name="15734"
|
><a name="15734"
|
||||||
|
|
@ -3161,6 +3288,22 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15757"
|
><a name="15757"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15758" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15759" href="Stlc.html#15759" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="15760"
|
||||||
|
> </a
|
||||||
|
><a name="15761" href="Stlc.html#15761" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="15762"
|
||||||
|
> </a
|
||||||
|
><a name="15763" href="Stlc.html#15763" class="Bound"
|
||||||
|
>z</a
|
||||||
|
><a name="15764" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15765"
|
||||||
|
> </a
|
||||||
><a name="15766" class="Symbol"
|
><a name="15766" class="Symbol"
|
||||||
>-></a
|
>-></a
|
||||||
><a name="15768"
|
><a name="15768"
|
||||||
|
|
@ -3839,7 +3982,7 @@ $$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
|
||||||
>=</a
|
>=</a
|
||||||
><a name="18109"
|
><a name="18109"
|
||||||
> </a
|
> </a
|
||||||
><a name="18110" href="Maps.html#9362" class="Function"
|
><a name="18110" href="Maps.html#9409" class="Function"
|
||||||
>PartialMap</a
|
>PartialMap</a
|
||||||
><a name="18120"
|
><a name="18120"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -3870,7 +4013,7 @@ $$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
|
||||||
>=</a
|
>=</a
|
||||||
><a name="18139"
|
><a name="18139"
|
||||||
> </a
|
> </a
|
||||||
><a name="18140" href="Maps.html#9495" class="Function"
|
><a name="18140" href="Maps.html#9542" class="Function"
|
||||||
>PartialMap.empty</a
|
>PartialMap.empty</a
|
||||||
><a name="18156"
|
><a name="18156"
|
||||||
>
|
>
|
||||||
|
|
@ -3892,7 +4035,7 @@ $$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
|
||||||
>-></a
|
>-></a
|
||||||
><a name="18173"
|
><a name="18173"
|
||||||
> </a
|
> </a
|
||||||
><a name="18174" href="Maps.html#2243" class="Datatype"
|
><a name="18174" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="18176"
|
><a name="18176"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -3921,7 +4064,7 @@ $$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
|
||||||
>=</a
|
>=</a
|
||||||
><a name="18200"
|
><a name="18200"
|
||||||
> </a
|
> </a
|
||||||
><a name="18201" href="Maps.html#9584" class="Function"
|
><a name="18201" href="Maps.html#9631" class="Function"
|
||||||
>PartialMap.update</a
|
>PartialMap.update</a
|
||||||
>
|
>
|
||||||
{% endraw %}</pre>
|
{% endraw %}</pre>
|
||||||
|
|
@ -4019,10 +4162,27 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19120"
|
><a name="19120"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19121" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19122" href="Stlc.html#19122" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19123" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19124"
|
||||||
|
> </a
|
||||||
><a name="19125" href="Stlc.html#19125" class="Bound"
|
><a name="19125" href="Stlc.html#19125" class="Bound"
|
||||||
>x</a
|
>x</a
|
||||||
><a name="19126"
|
><a name="19126"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19127" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19128" href="Stlc.html#19128" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="19129" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19130"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19147" class="Symbol"
|
><a name="19147" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19148"
|
><a name="19148"
|
||||||
|
|
@ -4089,6 +4249,47 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19213"
|
><a name="19213"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19214" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19215" href="Stlc.html#19215" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19216" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19217"
|
||||||
|
> </a
|
||||||
|
><a name="19218" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19219" href="Stlc.html#19219" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="19220" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19221"
|
||||||
|
> </a
|
||||||
|
><a name="19222" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19223" href="Stlc.html#19223" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="19224" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19225"
|
||||||
|
> </a
|
||||||
|
><a name="19226" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19227" href="Stlc.html#19227" class="Bound"
|
||||||
|
>B</a
|
||||||
|
><a name="19228" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19229"
|
||||||
|
> </a
|
||||||
|
><a name="19230" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19231" href="Stlc.html#19231" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="19232" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19233"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19250" class="Symbol"
|
><a name="19250" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19251"
|
><a name="19251"
|
||||||
|
|
@ -4187,6 +4388,47 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19329"
|
><a name="19329"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19330" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19331" href="Stlc.html#19331" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19332" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19333"
|
||||||
|
> </a
|
||||||
|
><a name="19334" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19335" href="Stlc.html#19335" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="19336" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19337"
|
||||||
|
> </a
|
||||||
|
><a name="19338" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19339" href="Stlc.html#19339" class="Bound"
|
||||||
|
>B</a
|
||||||
|
><a name="19340" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19341"
|
||||||
|
> </a
|
||||||
|
><a name="19342" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19343" href="Stlc.html#19343" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="19344" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19345"
|
||||||
|
> </a
|
||||||
|
><a name="19346" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19347" href="Stlc.html#19347" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="19348" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19349"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19366" class="Symbol"
|
><a name="19366" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19367"
|
><a name="19367"
|
||||||
|
|
@ -4290,6 +4532,15 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19463"
|
><a name="19463"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19464" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19465" href="Stlc.html#19465" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19466" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19467"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19484" class="Symbol"
|
><a name="19484" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19485"
|
><a name="19485"
|
||||||
|
|
@ -4327,6 +4578,15 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19522"
|
><a name="19522"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19523" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19524" href="Stlc.html#19524" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19525" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19526"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19543" class="Symbol"
|
><a name="19543" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19544"
|
><a name="19544"
|
||||||
|
|
@ -4364,6 +4624,47 @@ $$\Gamma$$."
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="19581"
|
><a name="19581"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19582" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19583" href="Stlc.html#19583" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19584" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19585"
|
||||||
|
> </a
|
||||||
|
><a name="19586" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19587" href="Stlc.html#19587" class="Bound"
|
||||||
|
>s</a
|
||||||
|
><a name="19588" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19589"
|
||||||
|
> </a
|
||||||
|
><a name="19590" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19591" href="Stlc.html#19591" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="19592" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19593"
|
||||||
|
> </a
|
||||||
|
><a name="19594" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19595" href="Stlc.html#19595" class="Bound"
|
||||||
|
>u</a
|
||||||
|
><a name="19596" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19597"
|
||||||
|
> </a
|
||||||
|
><a name="19598" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19599" href="Stlc.html#19599" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="19600" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19601"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="19618" class="Symbol"
|
><a name="19618" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="19619"
|
><a name="19619"
|
||||||
|
|
|
||||||
386
out/StlcProp.md
386
out/StlcProp.md
|
|
@ -55,7 +55,7 @@ permalink : /StlcProp
|
||||||
>;</a
|
>;</a
|
||||||
><a name="193"
|
><a name="193"
|
||||||
> </a
|
> </a
|
||||||
><a name="194" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
|
><a name="194" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function"
|
||||||
>⊥-elim</a
|
>⊥-elim</a
|
||||||
><a name="200" class="Symbol"
|
><a name="200" class="Symbol"
|
||||||
>)</a
|
>)</a
|
||||||
|
|
@ -460,6 +460,18 @@ $$false$$. For arrow types, the canonical forms are lambda-abstractions.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="1240"
|
><a name="1240"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="1241" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="1242" href="StlcProp.html#1242" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="1243"
|
||||||
|
> </a
|
||||||
|
><a name="1244" href="StlcProp.html#1244" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="1245" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="1246"
|
||||||
|
> </a
|
||||||
><a name="1247" class="Symbol"
|
><a name="1247" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="1248"
|
><a name="1248"
|
||||||
|
|
@ -630,6 +642,18 @@ first, then the formal version.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="1827"
|
><a name="1827"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="1828" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="1829" href="StlcProp.html#1829" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="1830"
|
||||||
|
> </a
|
||||||
|
><a name="1831" href="StlcProp.html#1831" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="1832" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="1833"
|
||||||
|
> </a
|
||||||
><a name="1834" class="Symbol"
|
><a name="1834" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="1835"
|
><a name="1835"
|
||||||
|
|
@ -1326,6 +1350,18 @@ instead of induction on typing derivations.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="4416"
|
><a name="4416"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="4417" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="4418" href="StlcProp.html#4418" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="4419"
|
||||||
|
> </a
|
||||||
|
><a name="4420" href="StlcProp.html#4420" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="4421" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="4422"
|
||||||
|
> </a
|
||||||
><a name="4423" class="Symbol"
|
><a name="4423" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="4424"
|
><a name="4424"
|
||||||
|
|
@ -1468,7 +1504,7 @@ Formally:
|
||||||
>:</a
|
>:</a
|
||||||
><a name="6920"
|
><a name="6920"
|
||||||
> </a
|
> </a
|
||||||
><a name="6921" href="Maps.html#2243" class="Datatype"
|
><a name="6921" href="Maps.html#2290" class="Datatype"
|
||||||
>Id</a
|
>Id</a
|
||||||
><a name="6923" class="Symbol"
|
><a name="6923" class="Symbol"
|
||||||
>)</a
|
>)</a
|
||||||
|
|
@ -1532,6 +1568,22 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="6978"
|
><a name="6978"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="6979" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="6980" href="StlcProp.html#6980" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="6981"
|
||||||
|
> </a
|
||||||
|
><a name="6982" href="StlcProp.html#6982" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="6983"
|
||||||
|
> </a
|
||||||
|
><a name="6984" href="StlcProp.html#6984" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="6985" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="6986"
|
||||||
|
> </a
|
||||||
><a name="6987" class="Symbol"
|
><a name="6987" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="6988"
|
><a name="6988"
|
||||||
|
|
@ -1605,6 +1657,18 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7039"
|
><a name="7039"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7040" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7041" href="StlcProp.html#7041" class="Bound"
|
||||||
|
>t₁</a
|
||||||
|
><a name="7043"
|
||||||
|
> </a
|
||||||
|
><a name="7044" href="StlcProp.html#7044" class="Bound"
|
||||||
|
>t₂</a
|
||||||
|
><a name="7046" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7047"
|
||||||
|
> </a
|
||||||
><a name="7048" class="Symbol"
|
><a name="7048" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7049"
|
><a name="7049"
|
||||||
|
|
@ -1658,6 +1722,18 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7093"
|
><a name="7093"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7094" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7095" href="StlcProp.html#7095" class="Bound"
|
||||||
|
>t₁</a
|
||||||
|
><a name="7097"
|
||||||
|
> </a
|
||||||
|
><a name="7098" href="StlcProp.html#7098" class="Bound"
|
||||||
|
>t₂</a
|
||||||
|
><a name="7100" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7101"
|
||||||
|
> </a
|
||||||
><a name="7102" class="Symbol"
|
><a name="7102" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7103"
|
><a name="7103"
|
||||||
|
|
@ -1711,6 +1787,22 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7147"
|
><a name="7147"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7148" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7149" href="StlcProp.html#7149" class="Bound"
|
||||||
|
>t₁</a
|
||||||
|
><a name="7151"
|
||||||
|
> </a
|
||||||
|
><a name="7152" href="StlcProp.html#7152" class="Bound"
|
||||||
|
>t₂</a
|
||||||
|
><a name="7154"
|
||||||
|
> </a
|
||||||
|
><a name="7155" href="StlcProp.html#7155" class="Bound"
|
||||||
|
>t₃</a
|
||||||
|
><a name="7157" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7158"
|
||||||
|
> </a
|
||||||
><a name="7159" class="Symbol"
|
><a name="7159" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7160"
|
><a name="7160"
|
||||||
|
|
@ -1780,6 +1872,22 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7218"
|
><a name="7218"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7219" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7220" href="StlcProp.html#7220" class="Bound"
|
||||||
|
>t₁</a
|
||||||
|
><a name="7222"
|
||||||
|
> </a
|
||||||
|
><a name="7223" href="StlcProp.html#7223" class="Bound"
|
||||||
|
>t₂</a
|
||||||
|
><a name="7225"
|
||||||
|
> </a
|
||||||
|
><a name="7226" href="StlcProp.html#7226" class="Bound"
|
||||||
|
>t₃</a
|
||||||
|
><a name="7228" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7229"
|
||||||
|
> </a
|
||||||
><a name="7230" class="Symbol"
|
><a name="7230" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7231"
|
><a name="7231"
|
||||||
|
|
@ -1849,6 +1957,22 @@ Formally:
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7289"
|
><a name="7289"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7290" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7291" href="StlcProp.html#7291" class="Bound"
|
||||||
|
>t₁</a
|
||||||
|
><a name="7293"
|
||||||
|
> </a
|
||||||
|
><a name="7294" href="StlcProp.html#7294" class="Bound"
|
||||||
|
>t₂</a
|
||||||
|
><a name="7296"
|
||||||
|
> </a
|
||||||
|
><a name="7297" href="StlcProp.html#7297" class="Bound"
|
||||||
|
>t₃</a
|
||||||
|
><a name="7299" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7300"
|
||||||
|
> </a
|
||||||
><a name="7301" class="Symbol"
|
><a name="7301" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7302"
|
><a name="7302"
|
||||||
|
|
@ -1946,6 +2070,14 @@ A term in which no variables appear free is said to be _closed_.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="7473"
|
><a name="7473"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="7474" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="7475" href="StlcProp.html#7475" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="7476" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="7477"
|
||||||
|
> </a
|
||||||
><a name="7478" class="Symbol"
|
><a name="7478" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="7479"
|
><a name="7479"
|
||||||
|
|
@ -1999,6 +2131,26 @@ $$\Gamma$$ assigns a type to $$x$$.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="8236"
|
><a name="8236"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="8237" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="8238" href="StlcProp.html#8238" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="8239"
|
||||||
|
> </a
|
||||||
|
><a name="8240" href="StlcProp.html#8240" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="8241"
|
||||||
|
> </a
|
||||||
|
><a name="8242" href="StlcProp.html#8242" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="8243"
|
||||||
|
> </a
|
||||||
|
><a name="8244" href="StlcProp.html#8244" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="8245" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="8246"
|
||||||
|
> </a
|
||||||
><a name="8247" class="Symbol"
|
><a name="8247" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="8248"
|
><a name="8248"
|
||||||
|
|
@ -2444,12 +2596,28 @@ _Proof_: We show, by induction on the proof that $$x$$ appears
|
||||||
>freeInCtxt</a
|
>freeInCtxt</a
|
||||||
><a name="10290"
|
><a name="10290"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="10291" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="10292" href="StlcProp.html#10292" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="10293" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="10294"
|
||||||
|
> </a
|
||||||
><a name="10295" class="Symbol"
|
><a name="10295" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="10296" href="StlcProp.html#6970" class="InductiveConstructor"
|
><a name="10296" href="StlcProp.html#6970" class="InductiveConstructor"
|
||||||
>abs</a
|
>abs</a
|
||||||
><a name="10299"
|
><a name="10299"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="10300" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="10301" href="StlcProp.html#10301" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="10302" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="10303"
|
||||||
|
> </a
|
||||||
><a name="10304" href="StlcProp.html#10304" class="Bound"
|
><a name="10304" href="StlcProp.html#10304" class="Bound"
|
||||||
>y≠x</a
|
>y≠x</a
|
||||||
><a name="10307"
|
><a name="10307"
|
||||||
|
|
@ -2511,7 +2679,7 @@ _Proof_: We show, by induction on the proof that $$x$$ appears
|
||||||
>y</a
|
>y</a
|
||||||
><a name="10371"
|
><a name="10371"
|
||||||
> </a
|
> </a
|
||||||
><a name="10372" href="Maps.html#2297" class="Function Operator"
|
><a name="10372" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="10373"
|
><a name="10373"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -2540,7 +2708,7 @@ _Proof_: We show, by induction on the proof that $$x$$ appears
|
||||||
>=</a
|
>=</a
|
||||||
><a name="10391"
|
><a name="10391"
|
||||||
> </a
|
> </a
|
||||||
><a name="10392" href="https://agda.github.io/agda-stdlib/Data.Empty.html#348" class="Function"
|
><a name="10392" href="https://agda.github.io/agda-stdlib/Data.Empty.html#360" class="Function"
|
||||||
>⊥-elim</a
|
>⊥-elim</a
|
||||||
><a name="10398"
|
><a name="10398"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -2605,6 +2773,18 @@ the empty context is closed (it has no free variables).
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="10651"
|
><a name="10651"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="10652" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="10653" href="StlcProp.html#10653" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="10654"
|
||||||
|
> </a
|
||||||
|
><a name="10655" href="StlcProp.html#10655" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="10656" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="10657"
|
||||||
|
> </a
|
||||||
><a name="10658" class="Symbol"
|
><a name="10658" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="10659"
|
><a name="10659"
|
||||||
|
|
@ -2656,6 +2836,18 @@ the empty context is closed (it has no free variables).
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="10741"
|
><a name="10741"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="10742" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="10743" href="StlcProp.html#10743" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="10744"
|
||||||
|
> </a
|
||||||
|
><a name="10745" href="StlcProp.html#10745" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="10746" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="10747"
|
||||||
|
> </a
|
||||||
><a name="10748" class="Symbol"
|
><a name="10748" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="10749"
|
><a name="10749"
|
||||||
|
|
@ -3051,6 +3243,14 @@ the empty context is closed (it has no free variables).
|
||||||
>)</a
|
>)</a
|
||||||
><a name="11229"
|
><a name="11229"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11230" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11231" href="StlcProp.html#11231" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="11232" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11233"
|
||||||
|
> </a
|
||||||
><a name="11234" class="Symbol"
|
><a name="11234" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="11235" href="StlcProp.html#6970" class="InductiveConstructor"
|
><a name="11235" href="StlcProp.html#6970" class="InductiveConstructor"
|
||||||
|
|
@ -3116,6 +3316,14 @@ the empty context is closed (it has no free variables).
|
||||||
>)</a
|
>)</a
|
||||||
><a name="11304"
|
><a name="11304"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11305" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11306" href="StlcProp.html#11306" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="11307" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11308"
|
||||||
|
> </a
|
||||||
><a name="11309" class="Symbol"
|
><a name="11309" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="11310" class="InductiveConstructor"
|
><a name="11310" class="InductiveConstructor"
|
||||||
|
|
@ -3156,7 +3364,7 @@ the empty context is closed (it has no free variables).
|
||||||
>x</a
|
>x</a
|
||||||
><a name="11340"
|
><a name="11340"
|
||||||
> </a
|
> </a
|
||||||
><a name="11341" href="Maps.html#2297" class="Function Operator"
|
><a name="11341" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="11342"
|
><a name="11342"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -3197,6 +3405,14 @@ the empty context is closed (it has no free variables).
|
||||||
>)</a
|
>)</a
|
||||||
><a name="11374"
|
><a name="11374"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11375" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11376" href="StlcProp.html#11376" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="11377" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11378"
|
||||||
|
> </a
|
||||||
><a name="11379" class="Symbol"
|
><a name="11379" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="11380" class="InductiveConstructor"
|
><a name="11380" class="InductiveConstructor"
|
||||||
|
|
@ -3286,6 +3502,14 @@ the empty context is closed (it has no free variables).
|
||||||
>)</a
|
>)</a
|
||||||
><a name="11453"
|
><a name="11453"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11454" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11455" href="StlcProp.html#11455" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="11456" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11457"
|
||||||
|
> </a
|
||||||
><a name="11458" class="Symbol"
|
><a name="11458" class="Symbol"
|
||||||
>(</a
|
>(</a
|
||||||
><a name="11459" class="InductiveConstructor"
|
><a name="11459" class="InductiveConstructor"
|
||||||
|
|
@ -3352,6 +3576,27 @@ is needed.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="11892"
|
><a name="11892"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11893" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11894" href="StlcProp.html#11894" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="11895"
|
||||||
|
> </a
|
||||||
|
><a name="11896" href="StlcProp.html#11896" class="Bound"
|
||||||
|
>Γ′</a
|
||||||
|
><a name="11898"
|
||||||
|
> </a
|
||||||
|
><a name="11899" href="StlcProp.html#11899" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="11900"
|
||||||
|
> </a
|
||||||
|
><a name="11901" href="StlcProp.html#11901" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="11902" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11903"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="11916" class="Symbol"
|
><a name="11916" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="11917"
|
><a name="11917"
|
||||||
|
|
@ -3360,6 +3605,14 @@ is needed.
|
||||||
>(∀</a
|
>(∀</a
|
||||||
><a name="11920"
|
><a name="11920"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="11921" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="11922" href="StlcProp.html#11922" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="11923" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="11924"
|
||||||
|
> </a
|
||||||
><a name="11925" class="Symbol"
|
><a name="11925" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="11926"
|
><a name="11926"
|
||||||
|
|
@ -3643,6 +3896,22 @@ $$\Gamma \vdash t \in T$$.
|
||||||
>replaceCtxt</a
|
>replaceCtxt</a
|
||||||
><a name="14466"
|
><a name="14466"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="14467" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14468" href="StlcProp.html#14468" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="14469" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14470"
|
||||||
|
> </a
|
||||||
|
><a name="14471" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14472" href="StlcProp.html#14472" class="Bound"
|
||||||
|
>Γ′</a
|
||||||
|
><a name="14474" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14475"
|
||||||
|
> </a
|
||||||
><a name="14476" href="StlcProp.html#14476" class="Bound"
|
><a name="14476" href="StlcProp.html#14476" class="Bound"
|
||||||
>f</a
|
>f</a
|
||||||
><a name="14477"
|
><a name="14477"
|
||||||
|
|
@ -3653,6 +3922,48 @@ $$\Gamma \vdash t \in T$$.
|
||||||
>abs</a
|
>abs</a
|
||||||
><a name="14482"
|
><a name="14482"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="14483" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14484" class="DottedPattern Symbol"
|
||||||
|
>.</a
|
||||||
|
><a name="14485" href="StlcProp.html#14468" class="DottedPattern Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="14486" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14487"
|
||||||
|
> </a
|
||||||
|
><a name="14488" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14489" href="StlcProp.html#14489" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="14490" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14491"
|
||||||
|
> </a
|
||||||
|
><a name="14492" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14493" href="StlcProp.html#14493" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="14494" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14495"
|
||||||
|
> </a
|
||||||
|
><a name="14496" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14497" href="StlcProp.html#14497" class="Bound"
|
||||||
|
>B</a
|
||||||
|
><a name="14498" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14499"
|
||||||
|
> </a
|
||||||
|
><a name="14500" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14501" href="StlcProp.html#14501" class="Bound"
|
||||||
|
>t′</a
|
||||||
|
><a name="14503" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14504"
|
||||||
|
> </a
|
||||||
><a name="14505" href="StlcProp.html#14505" class="Bound"
|
><a name="14505" href="StlcProp.html#14505" class="Bound"
|
||||||
>t′∶B</a
|
>t′∶B</a
|
||||||
><a name="14509" class="Symbol"
|
><a name="14509" class="Symbol"
|
||||||
|
|
@ -3702,6 +4013,14 @@ $$\Gamma \vdash t \in T$$.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="14559"
|
><a name="14559"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="14560" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14561" href="StlcProp.html#14561" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="14562" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14563"
|
||||||
|
> </a
|
||||||
><a name="14564" class="Symbol"
|
><a name="14564" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="14565"
|
><a name="14565"
|
||||||
|
|
@ -3787,6 +4106,14 @@ $$\Gamma \vdash t \in T$$.
|
||||||
>f′</a
|
>f′</a
|
||||||
><a name="14617"
|
><a name="14617"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="14618" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="14619" href="StlcProp.html#14619" class="Bound"
|
||||||
|
>y</a
|
||||||
|
><a name="14620" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="14621"
|
||||||
|
> </a
|
||||||
><a name="14622" href="StlcProp.html#14622" class="Bound"
|
><a name="14622" href="StlcProp.html#14622" class="Bound"
|
||||||
>y∈t′</a
|
>y∈t′</a
|
||||||
><a name="14626"
|
><a name="14626"
|
||||||
|
|
@ -3799,7 +4126,7 @@ $$\Gamma \vdash t \in T$$.
|
||||||
>x</a
|
>x</a
|
||||||
><a name="14633"
|
><a name="14633"
|
||||||
> </a
|
> </a
|
||||||
><a name="14634" href="Maps.html#2297" class="Function Operator"
|
><a name="14634" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="14635"
|
><a name="14635"
|
||||||
> </a
|
> </a
|
||||||
|
|
@ -4073,6 +4400,35 @@ $$\Gamma \vdash [x:=v]t : T$$.
|
||||||
>∀</a
|
>∀</a
|
||||||
><a name="15742"
|
><a name="15742"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="15743" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="15744" href="StlcProp.html#15744" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="15745"
|
||||||
|
> </a
|
||||||
|
><a name="15746" href="StlcProp.html#15746" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="15747"
|
||||||
|
> </a
|
||||||
|
><a name="15748" href="StlcProp.html#15748" class="Bound"
|
||||||
|
>A</a
|
||||||
|
><a name="15749"
|
||||||
|
> </a
|
||||||
|
><a name="15750" href="StlcProp.html#15750" class="Bound"
|
||||||
|
>t</a
|
||||||
|
><a name="15751"
|
||||||
|
> </a
|
||||||
|
><a name="15752" href="StlcProp.html#15752" class="Bound"
|
||||||
|
>v</a
|
||||||
|
><a name="15753"
|
||||||
|
> </a
|
||||||
|
><a name="15754" href="StlcProp.html#15754" class="Bound"
|
||||||
|
>B</a
|
||||||
|
><a name="15755" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="15756"
|
||||||
|
>
|
||||||
|
</a
|
||||||
><a name="15774" class="Symbol"
|
><a name="15774" class="Symbol"
|
||||||
>→</a
|
>→</a
|
||||||
><a name="15775"
|
><a name="15775"
|
||||||
|
|
@ -4280,6 +4636,22 @@ hand, _is_ completely generic.
|
||||||
>[:=]-preserves-⊢</a
|
>[:=]-preserves-⊢</a
|
||||||
><a name="19822"
|
><a name="19822"
|
||||||
> </a
|
> </a
|
||||||
|
><a name="19823" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19824" href="StlcProp.html#19824" class="Bound"
|
||||||
|
>Γ</a
|
||||||
|
><a name="19825" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19826"
|
||||||
|
> </a
|
||||||
|
><a name="19827" class="Symbol"
|
||||||
|
>{</a
|
||||||
|
><a name="19828" href="StlcProp.html#19828" class="Bound"
|
||||||
|
>x</a
|
||||||
|
><a name="19829" class="Symbol"
|
||||||
|
>}</a
|
||||||
|
><a name="19830"
|
||||||
|
> </a
|
||||||
><a name="19831" href="StlcProp.html#19831" class="Bound"
|
><a name="19831" href="StlcProp.html#19831" class="Bound"
|
||||||
>v∶A</a
|
>v∶A</a
|
||||||
><a name="19834"
|
><a name="19834"
|
||||||
|
|
@ -4308,7 +4680,7 @@ hand, _is_ completely generic.
|
||||||
>x</a
|
>x</a
|
||||||
><a name="19853"
|
><a name="19853"
|
||||||
> </a
|
> </a
|
||||||
><a name="19854" href="Maps.html#2297" class="Function Operator"
|
><a name="19854" href="Maps.html#2344" class="Function Operator"
|
||||||
>≟</a
|
>≟</a
|
||||||
><a name="19855"
|
><a name="19855"
|
||||||
> </a
|
> </a
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue