blob: 9c2979a6487376dddb729bb8d653a18cd6f15366 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
focus checkMetas: \[34ma[m -> ([32m\[32mb[m:Type -> [32mprimFix [32m[32ma[m[m [32m[32mb[m[m[m[m) (\[34ma[m:=[32mType[m [32mc[m:[32mType[m -> [47m<<HERE>>[m)
[32m\([34ma[m : [32m[32m[32mType[m~[32m[32mV0[m[m[m[m) ([34mb[m : [32m[32m[32m[32mV1[m[m~[32m'X[m[m[m) -> [32m[32mtypeAnn [32m[32mV2[m[m ([32m[32mlabend [32mX[m[m[m)[m[m[m
------------ trace
'X :: [32mType[39m[K
X :: [32m'X[39m[K
'XCase :: [32m(b : 'X->Type) -> b X -> d:'X -> b d[39m[K
match'X :: [32m(b : Type->Type) -> b 'X -> d:Type -> b d -> b d[39m[K
!focus checkMetas: \[34ma[m -> ([32m\[32mb[m:Type -> [32mprimFix [32m[32ma[m[m [32m[32mb[m[m[m[m) (\[34ma[m:=[32mType[m [32mc[m:[32mType[m -> [47m<<HERE>>[m)
[32m\([34ma[m : [32m[32m[32mType[m~[32m[32mV0[m[m[m[m) ([34mb[m : [32m[32m[32m[32mV1[m[m~[32m'X[m[m[m) -> [32m[32mtypeAnn [32m[32mV2[m[m ([32m[32mlabend [32mX[m[m[m)[m[m[m
------------ tooltips
testdata/typesig.reject.lc 4:6-4:7 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 V1
testdata/typesig.reject.lc 6:6-7:6 V0->V1 | V2
testdata/typesig.reject.lc 7:5-7:6 X
|
