blob: 5241517a8d2aeca0c457d5ee59e1457e1cfb319f (
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
| ^^^ this expects an argument of type: Kind
| ^ but this has type: Sort
|
|
