blob: eb004b932bebf02766b706683c3913facc8dc446 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
main is not found
------------ trace
id :: [32m{a} -> a->a[39m[K
'X :: [32m{a} -> a->Type[39m[K
'XCase :: [32m{a} -> {b:a} -> (d : 'X a b -> Type) -> (e : 'X a b) -> d e[39m[K
match'X :: [32m(b : Type->Type) -> ({c} -> d:c -> b ('X c d)) -> f:Type -> b f -> b f[39m[K
x :: [32m'X (Type -> Type->Type) (\c:Type d:Type -> (c, d))[39m[K
------------ tooltips
testdata/traceTest.lc 6:1-6:3 {a} -> a->a
testdata/traceTest.lc 6:8-6:9 V1
testdata/traceTest.lc 8:6-8:7 Type | {a} -> a->Type
testdata/traceTest.lc 8:6-8:18 Type
testdata/traceTest.lc 8:17-8:18 Type
testdata/traceTest.lc 10:6-10:7 {a} -> a->Type
testdata/traceTest.lc 10:6-10:25 Type
testdata/traceTest.lc 10:19-10:20 V4
testdata/traceTest.lc 10:19-10:23 List Type
testdata/traceTest.lc 10:22-10:23 List Type | V2
testdata/traceTest.lc 11:1-11:2 X (Type -> Type->Type) (\c:Type d:Type -> (c, d))
testdata/traceTest.lc 11:5-11:14 {a}->a
|
