blob: 2480480165203fbef9276b0c502d8983eb1d0f70 (
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
6:1-6:3
forall a . a -> a
6:8-6:9
_b
8:6-8:7
forall a . a -> Type | forall a . a -> Type | forall a . a -> Type | Type | Type
8:6-8:18
Type
8:17-8:18
Type | Type | Type
10:6-10:7
forall a . a -> Type
10:6-10:25
Type
10:17-10:24
Type
10:19-10:20
_e
10:19-10:23
[Type]
10:22-10:23
_c | [Type]
11:1-11:2
X (Type -> Type -> Type) \a b -> (a, b)
11:5-11:14
forall a . a
|
