blob: e06c4b2dd6488a148ea121e657e784e11c8ae106 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Type error: Unhandled error: error: Wrong type of function argument
--> <current file>:6:23
|
1 | let bottom : Type = ∀(any : Type) → any
2 |
3 | in let not : Type → Type = λ(p : Type) → p → bottom
4 |
...
10 | : pow (pow U) → U
11 | = λ(t : pow (pow U))
| ^^^^^ Wrong type of function argument
| --- help: this expects an argument of type: Kind
| - help: but this has type: Sort
|
|