blob: 8d18a7f352a32b9aa1ae90710f02fe0f208c9f10 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
focus checkMetas: labEnd \{[32ma[m}->[47m<<HERE>>[m
[32m\([34ma[m : [32m[32m[32m[32mV0[m[m~[32m'X[m[m[m)->[32mX[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: labEnd \{[32ma[m}->[47m<<HERE>>[m
[32m\([34ma[m : [32m[32m[32m[32mV0[m[m~[32m'X[m[m[m)->[32mX[m[m
------------ tooltips
testdata/typesig.reject.lc 3:6-3:7 Type
testdata/typesig.reject.lc 3:6-3:11 Type
testdata/typesig.reject.lc 3:10-3:11 X
testdata/typesig.reject.lc 5:6-5:7 Type | V1
testdata/typesig.reject.lc 6:5-6:6 X
|
