blob: 90566f2c1b5b5ee4147162104372244257b366f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
focus checkMetas: \(a :: Type) -> (\(b :: Type) -> primFix a b)
\(a := Type) -> \(c :: Type) -> <<HERE>>
\(a :: Type ~ _a) (b :: _a ~ X) -> typeAnn _a (labend X)
------------ trace
'X :: Type
X :: X
'XCase :: forall (a :: X -> Type) -> a 'X -> forall (b :: X) -> a b
match'X :: forall (a :: Type -> Type) -> a X -> forall b -> a b -> a b
!focus checkMetas: \(a :: Type) -> (\(b :: Type) -> primFix a b)
\(a := Type) -> \(c :: Type) -> <<HERE>>
\(a :: Type ~ _a) (b :: _a ~ X) -> typeAnn _a (labend X)
------------ tooltips
testdata/typesig.reject.lc 4:6-4:7
Type | Type | Type | Type | Type
testdata/typesig.reject.lc 4:6-4:11
Type
testdata/typesig.reject.lc 4:10-4:11
X
testdata/typesig.reject.lc 6:6-6:7
_b
testdata/typesig.reject.lc 6:6-7:6
_c
testdata/typesig.reject.lc 7:5-7:6
X
|
