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

Lambda: fix the term in an example showing typing relation is not injective

Browse source
This commit is contained in:
Marko Dimjašević 2020-01-03 08:50:22 +01:00
parent 233bac8071
commit 3a3539bb77
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/Lambda.lagda.md
View file

@ -1315,7 +1315,7 @@ there is at most one `A` such that the judgment holds:
```
The typing relation `Γ ⊢ M ⦂ A` is not injective. For example, in any `Γ`
the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`.
the term `` ƛ "x" ⇒ ` "x" `` has type `A ⇒ A` for any type `A`.
### Non-examples