File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed
Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -34,7 +34,7 @@ Pull requests are encouraged.
3434
3535 - [ Lambda] ({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
3636 - [ Properties] ({{ site.baseurl }}/Properties/): Progress and Preservation
37- - [ DeBruijn] ({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
37+ - [ DeBruijn] ({{ site.baseurl }}/DeBruijn/): Intrinsically- typed de Bruijn representation
3838 - [ More] ({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
3939 - [ Bisimulation] ({{ site.baseurl }}/Bisimulation/): Relating reductions systems
4040 - [ Inference] ({{ site.baseurl }}/Inference/): Bidirectional type inference
Original file line number Diff line number Diff line change @@ -33,7 +33,7 @@ Pull requests are encouraged.
3333
3434 - [ Lambda] ({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
3535 - [ Properties] ({{ site.baseurl }}/Properties/): Progress and Preservation
36- - [ DeBruijn] ({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
36+ - [ DeBruijn] ({{ site.baseurl }}/DeBruijn/): Intrinsically- typed de Bruijn representation
3737 - [ More] ({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
3838 - [ Bisimulation] ({{ site.baseurl }}/Bisimulation/): Relating reductions systems
3939 - [ Inference] ({{ site.baseurl }}/Inference/): Bidirectional type inference
Original file line number Diff line number Diff line change @@ -61,7 +61,7 @@ open import plfa.part3.Compositional using (lambda-inversion; var-inv)
6161The proof of preservation in this section mixes techniques from
6262previous chapters. Like the proof of preservation for the STLC, we are
6363preserving a relation defined separately from the syntax, in contrast
64- to the inherently typed terms. On the other hand, we are using de
64+ to the intrinsically- typed terms. On the other hand, we are using de
6565Bruijn indices for variables.
6666
6767The outline of the proof remains the same in that we must prove lemmas
You can’t perform that action at this time.
0 commit comments