blob: 5aacb809d0dee185b5a92d9d443c636db9cf1da5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Type error: error: wrong type of function argument
--> <current file>:6:15
|
1 | let bottom : Type = ∀(any : Type) → any
2 |
3 | in let not : Type → Type = λ(p : Type) → p → bottom
4 |
...
9 | in let tau
10 | : pow (pow U) → U
| ^^^ this expects an argument of type: Kind
| ^ but this has type: Sort
|
= note: expected type `Kind`
found type `Sort`
|
