blob: 522e1a2261f172c68c38a667c3863da712c81ced (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
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))
| ^^^ this expects an argument of type: Kind
| ^ but this has type: Sort
|
= note: expected type `Kind`
found type `Sort`
|
