blob: 6e360da1c4e69216ed71b850c836c7d1e32c40a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Type error: error: expected function, found `Natural`
--> <current file>:6:25
|
1 | -- When you check if an inferred type is equivalent to an annotation,
2 | -- you must alpha-beta-normalize both sides first. But it is not safe
3 | -- to beta-normalise an expression which hasn't first been
4 | -- typechecked.
...
10 | let a
11 | : (λ(x : Natural) → x x) (λ(x : Natural) → x x)
| ^ function application requires a function
|
|
