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

Merge pull request #557 from asr/typos

Browse source 
Fixed typos in the grammar for inherited terms
This commit is contained in:
Philip Wadler 2021-02-10 17:00:03 +00:00 committed by GitHub
commit 045f66a7bc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/part2/Inference.lagda.md
View file

@ -191,12 +191,12 @@ We can extract the grammar for terms from the above:
M⁻ ↓ A switch to inherited M⁻ ↓ A switch to inherited
L⁻, M⁻, N⁻ ::= terms with inherited type L⁻, M⁻, N⁻ ::= terms with inherited type
ƛ x ⇒ N abstraction ƛ x ⇒ N⁻ abstraction
`zero zero `zero zero
`suc M⁻ successor `suc M⁻ successor
case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ] case case L⁺ [zero⇒ M⁻ |suc x ⇒ N⁻ ] case
μ x ⇒ N fixpoint μ x ⇒ N⁻ fixpoint
M ↑ switch to synthesized M⁺ ↑ switch to synthesized
We will formalise the above shortly. We will formalise the above shortly.