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

Changed missed inherent occurrences to intrinsic

Browse source
This commit is contained in:
Reza Gharibi 2019-09-01 01:56:51 +04:30 committed by Wen Kokke
parent 3ef66e5dbe
commit 63fcbbe25e
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
beta.md
View file

@ -34,7 +34,7 @@ Pull requests are encouraged.
- [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
- [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
- [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference

2
index.md
View file

@ -33,7 +33,7 @@ Pull requests are encouraged.
- [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
- [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
- [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference

2
src/plfa/part3/Soundness.lagda.md
View file

@ -61,7 +61,7 @@ open import plfa.part3.Compositional using (lambda-inversion; var-inv)
The proof of preservation in this section mixes techniques from
previous chapters. Like the proof of preservation for the STLC, we are
preserving a relation defined separately from the syntax, in contrast
to the inherently typed terms. On the other hand, we are using de
to the intrinsically-typed terms. On the other hand, we are using de
Bruijn indices for variables.
The outline of the proof remains the same in that we must prove lemmas