blob: 10bb9a4b31764505f43cf5fa9013348183b2e64d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Type error: Unhandled error: error: function annot mismatch
--> <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))
| ^^^^^ function annot mismatch
| --- help: this expects an argument of type: Kind
| - help: but this has type: Sort
|
|
