blob: 215f950a2b2903e6cf7f9ad1f4ad1574b8e5eaf4 (
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
main is not found
------------ desugared source code
id = _lhs id \(a :: _) -> _rhs a
data X (_ :: Type) (_ :: _a) :: Type where
x :: X \(a :: _) (b :: _) -> (a, b)
x = _lhs x (_rhs undefined)
------------ core code
'X :: forall a . a -> Type
'X = <<type constructor with 0 indices; constructors: >>
case'X :: forall a (b :: a) . forall (c :: X a b -> Type) (d :: X a b) -> c d
case'X = \_ _ a b -> <<case function of a type with 2 parameters>>
id :: forall a . a -> a
id = \a b -> _rhs b
match'X
:: forall (a :: Type -> Type)
-> (forall b . forall (c :: b) -> a (X b c)) -> forall d -> a d -> a d
match'X = \a b c d -> <<type case function>>
x :: X (Type -> Type -> Type) \a b -> (a, b)
x = _rhs (undefined ('X (Type -> Type -> Type) \a b -> ' (a, b)))
------------ tooltips
testdata/traceTest.lc 6:1-6:3
forall a . a -> a
testdata/traceTest.lc 6:8-6:9
_b
testdata/traceTest.lc 8:6-8:7
forall a . a -> Type | forall a . a -> Type | forall a . a -> Type | Type | Type
testdata/traceTest.lc 8:6-8:18
Type
testdata/traceTest.lc 8:17-8:18
Type | Type | Type
testdata/traceTest.lc 10:6-10:7
forall a . a -> Type
testdata/traceTest.lc 10:6-10:25
Type
testdata/traceTest.lc 10:17-10:24
Type
testdata/traceTest.lc 10:19-10:20
_e
testdata/traceTest.lc 10:19-10:23
[Type]
testdata/traceTest.lc 10:22-10:23
_c | [Type]
testdata/traceTest.lc 11:1-11:2
X (Type -> Type -> Type) \a b -> (a, b)
testdata/traceTest.lc 11:5-11:14
forall a . a
|