main is not found ------------ trace typeAnn :: {a} -> a->a parens :: {a} -> a->a undefined :: {a}->a primFix :: {a} -> a->a -> a 'Unit :: Type TT :: 'Unit 'UnitCase :: (b : 'Unit->Type) -> b TT -> d:'Unit -> b d match'Unit :: (b : Type->Type) -> b 'Unit -> d:Type -> b d -> b d 'String :: Type 'StringCase :: (b : 'String->Type) -> c:'String -> b c match'String :: (b : Type->Type) -> b 'String -> d:Type -> b d -> b d 'Empty :: 'String->Type 'EmptyCase :: {a:'String} -> (c : 'Empty a -> Type) -> (d : 'Empty a) -> c d match'Empty :: (b : Type->Type) -> (c:'String -> b ('Empty c)) -> e:Type -> b e -> b e unsafeCoerce :: {a} -> {b} -> a->b 'EqCT :: a:Type -> a -> a->Type parEval :: a:Type -> a -> a->a 'T2 :: Type -> Type->Type match'Type :: (b : Type->Type) -> b Type -> d:Type -> b d -> b d 'EqCTt :: {a} -> a -> a->Type t2C :: 'Unit -> 'Unit->'Unit 'Int :: Type 'IntCase :: (b : 'Int->Type) -> c:'Int -> b c match'Int :: (b : Type->Type) -> b 'Int -> d:Type -> b d -> b d 'Word :: Type 'WordCase :: (b : 'Word->Type) -> c:'Word -> b c match'Word :: (b : Type->Type) -> b 'Word -> d:Type -> b d -> b d 'Float :: Type 'FloatCase :: (b : 'Float->Type) -> c:'Float -> b c match'Float :: (b : Type->Type) -> b 'Float -> d:Type -> b d -> b d 'Char :: Type 'CharCase :: (b : 'Char->Type) -> c:'Char -> b c match'Char :: (b : Type->Type) -> b 'Char -> d:Type -> b d -> b d 'Bool :: Type False :: 'Bool True :: 'Bool 'BoolCase :: (b : 'Bool->Type) -> b False -> b True -> e:'Bool -> b e match'Bool :: (b : Type->Type) -> b 'Bool -> d:Type -> b d -> b d 'Ordering :: Type LT :: 'Ordering EQ :: 'Ordering GT :: 'Ordering 'OrderingCase :: (b : 'Ordering->Type) -> b LT -> b EQ -> b GT -> f:'Ordering -> b f match'Ordering :: (b : Type->Type) -> b 'Ordering -> d:Type -> b d -> b d 'Nat :: Type Zero :: 'Nat Succ :: 'Nat->'Nat 'NatCase :: (b : 'Nat->Type) -> b 0 -> (d:'Nat -> b (Succ d)) -> f:'Nat -> b f match'Nat :: (b : Type->Type) -> b 'Nat -> d:Type -> b d -> b d primIntToWord :: 'Int->'Word primIntToFloat :: 'Int->'Float primIntToNat :: 'Int->'Nat primCompareInt :: 'Int -> 'Int->'Ordering primCompareWord :: 'Word -> 'Word->'Ordering primCompareFloat :: 'Float -> 'Float->'Ordering primCompareChar :: 'Char -> 'Char->'Ordering primCompareString :: 'String -> 'String->'Ordering primNegateInt :: 'Int->'Int primNegateWord :: 'Word->'Word primNegateFloat :: 'Float->'Float primAddInt :: 'Int -> 'Int->'Int primSubInt :: 'Int -> 'Int->'Int primModInt :: 'Int -> 'Int->'Int primSqrtFloat :: 'Float->'Float primRound :: 'Float->'Int primIfThenElse :: {a} -> 'Bool -> a -> a->a isEQ :: 'Ordering->'Bool 'Num :: Type->Type fromInt :: {a} -> {b : 'Num a} -> 'Int->a compare :: {a} -> {b : 'Num a} -> a -> a->'Ordering negate :: {a} -> {b : 'Num a} -> a->a 'Eq :: Type->Type == :: {a} -> {b : 'Eq a} -> a -> a->'Bool 'List :: Type->Type Nil :: {a} -> 'List a Cons :: {a} -> a -> 'List a -> 'List a 'ListCase :: {a} -> (c : 'List a -> Type) -> c Nil -> (e:a -> (f : 'List a) -> c (Cons e f)) -> (h : 'List a) -> c h match'List :: (b : Type->Type) -> (c:Type -> b ('List c)) -> e:Type -> b e -> b e 'HList :: 'List Type -> Type HNil :: () HCons :: {a} -> {b : 'List Type} -> a -> 'HList b -> 'HList (Cons a b) 'HListCase :: (c : (a : 'List Type) -> 'HList a -> Type) -> c Nil () -> ({e} -> {f : 'List Type} -> g:e -> (h : 'HList f) -> c (Cons e f) (HCons e f g h)) -> {j : 'List Type} -> (k : 'HList j) -> c j k match'HList :: (b : Type->Type) -> ((c : 'List Type) -> b ('HList c)) -> e:Type -> b e -> b e hlistNilCase :: a:Type -> a -> ()->a hlistConsCase :: {a} -> {b : 'List Type} -> c:Type -> (a -> 'HList b -> c) -> 'HList (Cons a b) -> c ------------ tooltips testdata/Internals.lc 6:1-6:8 {a} -> a->a testdata/Internals.lc 6:13-6:14 V1 testdata/Internals.lc 9:1-9:7 {a} -> a->a testdata/Internals.lc 9:12-9:13 V1 testdata/Internals.lc 11:1-11:10 {a}->a testdata/Internals.lc 11:27-11:31 Type testdata/Internals.lc 11:35-11:36 Type testdata/Internals.lc 13:1-13:8 {a} -> a->a -> a testdata/Internals.lc 13:25-13:29 Type testdata/Internals.lc 13:33-13:46 Type testdata/Internals.lc 13:34-13:35 Type testdata/Internals.lc 13:39-13:40 Type testdata/Internals.lc 13:45-13:46 Type testdata/Internals.lc 15:6-15:10 Type testdata/Internals.lc 15:6-15:15 Type testdata/Internals.lc 15:13-15:15 Unit testdata/Internals.lc 16:6-16:12 Type testdata/Internals.lc 17:6-17:11 String->Type | Type testdata/Internals.lc 17:18-17:24 Type testdata/Internals.lc 19:1-19:13 {a} -> {b} -> a->b testdata/Internals.lc 19:30-19:31 V3 testdata/Internals.lc 19:30-19:36 Type testdata/Internals.lc 19:35-19:36 Type | V2 testdata/Internals.lc 22:13-22:17 a:Type -> a -> a->Type testdata/Internals.lc 22:24-22:28 Type testdata/Internals.lc 22:36-22:37 Type testdata/Internals.lc 22:36-22:46 Type testdata/Internals.lc 22:45-22:46 Type testdata/Internals.lc 31:1-31:8 a:Type -> a -> a->a testdata/Internals.lc 31:24-31:25 V1 testdata/Internals.lc 31:24-31:35 Type testdata/Internals.lc 31:29-31:30 Type testdata/Internals.lc 31:29-31:35 Type testdata/Internals.lc 31:34-31:35 Type testdata/Internals.lc 34:13-34:15 Type -> Type->Type testdata/Internals.lc 36:1-36:11 (b : Type->Type) -> b Type -> d:Type -> b d -> b d testdata/Internals.lc 36:28-36:32 Type testdata/Internals.lc 36:36-36:40 Type testdata/Internals.lc 36:45-36:46 Type->Type testdata/Internals.lc 36:45-36:51 Type testdata/Internals.lc 36:45-36:87 Type testdata/Internals.lc 36:47-36:51 Type testdata/Internals.lc 36:55-36:87 Type testdata/Internals.lc 36:68-36:72 Type testdata/Internals.lc 36:77-36:78 Type->Type testdata/Internals.lc 36:77-36:80 Type testdata/Internals.lc 36:77-36:87 Type testdata/Internals.lc 36:79-36:80 Type testdata/Internals.lc 36:84-36:85 Type->Type testdata/Internals.lc 36:84-36:87 Type testdata/Internals.lc 36:86-36:87 Type testdata/Internals.lc 38:6-38:11 {a} -> a -> a->Type testdata/Internals.lc 38:14-38:18 a:Type -> a -> a->Type testdata/Internals.lc 38:14-38:20 V0 -> V1->Type testdata/Internals.lc 41:1-41:4 Unit -> Unit->Unit testdata/Internals.lc 41:8-41:12 Type testdata/Internals.lc 41:16-41:20 Type testdata/Internals.lc 41:16-41:28 Type testdata/Internals.lc 41:24-41:28 Type testdata/Internals.lc 44:6-44:9 Type testdata/Internals.lc 45:6-45:10 Type testdata/Internals.lc 46:6-46:11 Type testdata/Internals.lc 47:6-47:10 Type testdata/Internals.lc 49:6-49:10 Type testdata/Internals.lc 49:6-49:25 Type testdata/Internals.lc 49:13-49:18 Bool testdata/Internals.lc 49:21-49:25 Bool testdata/Internals.lc 51:6-51:14 Type testdata/Internals.lc 51:6-51:29 Type testdata/Internals.lc 51:17-51:19 Ordering testdata/Internals.lc 51:22-51:24 Ordering testdata/Internals.lc 51:27-51:29 Ordering testdata/Internals.lc 53:6-53:9 Type testdata/Internals.lc 53:6-53:23 Type testdata/Internals.lc 53:12-53:16 Nat testdata/Internals.lc 53:19-53:23 Nat | Nat->Nat | Type testdata/Internals.lc 53:24-53:27 Type testdata/Internals.lc 56:1-56:14 Int->Word testdata/Internals.lc 56:24-56:27 Type testdata/Internals.lc 56:33-56:37 Type testdata/Internals.lc 57:1-57:15 Int->Float testdata/Internals.lc 57:24-57:27 Type testdata/Internals.lc 57:33-57:38 Type testdata/Internals.lc 58:1-58:13 Int->Nat testdata/Internals.lc 58:24-58:27 Type testdata/Internals.lc 58:33-58:36 Type testdata/Internals.lc 59:1-59:15 Int -> Int->Ordering testdata/Internals.lc 59:24-59:27 Type testdata/Internals.lc 59:33-59:36 Type testdata/Internals.lc 59:33-59:50 Type testdata/Internals.lc 59:42-59:50 Type testdata/Internals.lc 60:1-60:16 Word -> Word->Ordering testdata/Internals.lc 60:24-60:28 Type testdata/Internals.lc 60:33-60:37 Type testdata/Internals.lc 60:33-60:50 Type testdata/Internals.lc 60:42-60:50 Type testdata/Internals.lc 61:1-61:17 Float -> Float->Ordering testdata/Internals.lc 61:24-61:29 Type testdata/Internals.lc 61:33-61:38 Type testdata/Internals.lc 61:33-61:50 Type testdata/Internals.lc 61:42-61:50 Type testdata/Internals.lc 62:1-62:16 Char -> Char->Ordering testdata/Internals.lc 62:24-62:28 Type testdata/Internals.lc 62:33-62:37 Type testdata/Internals.lc 62:33-62:50 Type testdata/Internals.lc 62:42-62:50 Type testdata/Internals.lc 63:1-63:18 String -> String->Ordering testdata/Internals.lc 63:24-63:30 Type testdata/Internals.lc 63:34-63:40 Type testdata/Internals.lc 63:34-63:52 Type testdata/Internals.lc 63:44-63:52 Type testdata/Internals.lc 64:1-64:14 Int->Int testdata/Internals.lc 64:24-64:27 Type testdata/Internals.lc 64:33-64:36 Type testdata/Internals.lc 65:1-65:15 Word->Word testdata/Internals.lc 65:24-65:28 Type testdata/Internals.lc 65:33-65:37 Type testdata/Internals.lc 66:1-66:16 Float->Float testdata/Internals.lc 66:24-66:29 Type testdata/Internals.lc 66:33-66:38 Type testdata/Internals.lc 67:1-67:11 Int -> Int->Int testdata/Internals.lc 67:24-67:27 Type testdata/Internals.lc 67:33-67:36 Type testdata/Internals.lc 67:33-67:45 Type testdata/Internals.lc 67:42-67:45 Type testdata/Internals.lc 68:1-68:11 Int -> Int->Int testdata/Internals.lc 68:24-68:27 Type testdata/Internals.lc 68:33-68:36 Type testdata/Internals.lc 68:33-68:45 Type testdata/Internals.lc 68:42-68:45 Type testdata/Internals.lc 69:1-69:11 Int -> Int->Int testdata/Internals.lc 69:24-69:27 Type testdata/Internals.lc 69:33-69:36 Type testdata/Internals.lc 69:33-69:45 Type testdata/Internals.lc 69:42-69:45 Type testdata/Internals.lc 70:1-70:14 Float->Float testdata/Internals.lc 70:24-70:29 Type testdata/Internals.lc 70:33-70:38 Type testdata/Internals.lc 71:1-71:10 Float->Int testdata/Internals.lc 71:24-71:29 Type testdata/Internals.lc 71:33-71:36 Type testdata/Internals.lc 74:19-74:23 Type testdata/Internals.lc 74:19-74:38 Type testdata/Internals.lc 74:27-74:28 V2 testdata/Internals.lc 74:27-74:38 Type testdata/Internals.lc 74:32-74:33 Type testdata/Internals.lc 74:32-74:38 Type testdata/Internals.lc 74:37-74:38 Type testdata/Internals.lc 75:1-75:15 {a} -> Bool -> a -> a->a testdata/Internals.lc 75:16-75:20 Bool testdata/Internals.lc 75:16-76:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3 testdata/Internals.lc 75:28-75:29 V3 testdata/Internals.lc 75:28-76:29 Bool->V4 testdata/Internals.lc 76:28-76:29 V4 testdata/Internals.lc 78:1-78:5 Ordering->Bool testdata/Internals.lc 78:6-78:8 V1 testdata/Internals.lc 78:6-79:15 Bool testdata/Internals.lc 78:11-78:15 Bool testdata/Internals.lc 78:11-79:15 Bool -> Ordering->Bool testdata/Internals.lc 79:10-79:15 Bool testdata/Internals.lc 82:7-82:10 Type->Type testdata/Internals.lc 82:7-83:22 Type testdata/Internals.lc 82:7-84:32 Type testdata/Internals.lc 82:7-85:19 Type testdata/Internals.lc 83:3-83:10 {a} -> {b : Num a} -> Int->a testdata/Internals.lc 83:14-83:17 Type testdata/Internals.lc 83:14-83:22 Type testdata/Internals.lc 83:21-83:22 Type testdata/Internals.lc 84:3-84:10 {a} -> {b : Num a} -> a -> a->Ordering testdata/Internals.lc 84:14-84:15 Type testdata/Internals.lc 84:14-84:32 Type testdata/Internals.lc 84:19-84:20 Type testdata/Internals.lc 84:19-84:32 Type testdata/Internals.lc 84:24-84:32 Type testdata/Internals.lc 85:3-85:9 {a} -> {b : Num a} -> a->a testdata/Internals.lc 85:13-85:14 Type testdata/Internals.lc 85:13-85:19 Type testdata/Internals.lc 85:18-85:19 Type testdata/Internals.lc 87:14-87:17 Type testdata/Internals.lc 87:14-88:20 Int->V2 -> Int->V3 testdata/Internals.lc 87:14-89:27 (V1 -> V2->Ordering) -> V2 -> V3->Ordering testdata/Internals.lc 87:14-90:26 V1->V2 -> V2->V3 testdata/Internals.lc 87:14-99:17 Type | Type->Type testdata/Internals.lc 87:14-100:25 Int->V2 | {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a testdata/Internals.lc 87:14-101:22 V1 -> V2->Ordering | {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering testdata/Internals.lc 87:14-102:22 V1->V2 | {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a testdata/Internals.lc 88:19-88:20 V1 testdata/Internals.lc 89:13-89:27 Int -> Int->Ordering testdata/Internals.lc 90:13-90:26 Int->Int testdata/Internals.lc 91:14-91:18 Type testdata/Internals.lc 91:14-92:26 Int->V2 -> Int->V3 testdata/Internals.lc 91:14-93:28 (V1 -> V2->Ordering) -> V2 -> V3->Ordering testdata/Internals.lc 91:14-94:27 V1->V2 -> V2->V3 testdata/Internals.lc 91:14-99:17 Type testdata/Internals.lc 91:14-100:25 Int->V2 testdata/Internals.lc 91:14-101:22 V1 -> V2->Ordering testdata/Internals.lc 91:14-102:22 V1->V2 testdata/Internals.lc 92:13-92:26 Int->Word testdata/Internals.lc 93:13-93:28 Word -> Word->Ordering testdata/Internals.lc 94:13-94:27 Word->Word testdata/Internals.lc 95:14-95:19 Type testdata/Internals.lc 95:14-96:27 Int->V2 -> Int->V3 testdata/Internals.lc 95:14-97:29 (V1 -> V2->Ordering) -> V2 -> V3->Ordering testdata/Internals.lc 95:14-98:28 V1->V2 -> V2->V3 testdata/Internals.lc 95:14-99:17 Type testdata/Internals.lc 95:14-100:25 Int->V2 testdata/Internals.lc 95:14-101:22 V1 -> V2->Ordering testdata/Internals.lc 95:14-102:22 V1->V2 testdata/Internals.lc 96:13-96:27 Int->Float testdata/Internals.lc 97:13-97:29 Float -> Float->Ordering testdata/Internals.lc 98:13-98:28 Float->Float testdata/Internals.lc 99:14-99:17 Type testdata/Internals.lc 99:14-100:25 Int->V2 -> Int->V3 testdata/Internals.lc 99:14-101:22 (V1 -> V2->Ordering) -> V2 -> V3->Ordering testdata/Internals.lc 99:14-102:22 V1->V2 -> V2->V3 testdata/Internals.lc 100:13-100:25 Int->Nat testdata/Internals.lc 101:13-101:22 {a}->a testdata/Internals.lc 102:13-102:22 {a}->a testdata/Internals.lc 104:7-104:9 Type->Type testdata/Internals.lc 104:7-105:27 Type testdata/Internals.lc 104:7-120:29 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool testdata/Internals.lc 105:6-105:8 {a} -> {b : Eq a} -> a -> a->Bool testdata/Internals.lc 105:13-105:14 Type testdata/Internals.lc 105:13-105:27 Type testdata/Internals.lc 105:18-105:19 Type testdata/Internals.lc 105:18-105:27 Type testdata/Internals.lc 105:23-105:27 Type testdata/Internals.lc 109:13-109:19 Type testdata/Internals.lc 109:13-109:63 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 109:13-117:16 Type | Type->Type testdata/Internals.lc 109:13-120:29 V1 -> V2->Bool | {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool testdata/Internals.lc 109:35-109:39 Ordering->Bool testdata/Internals.lc 109:35-109:63 Bool testdata/Internals.lc 109:41-109:58 String -> String->Ordering testdata/Internals.lc 109:41-109:60 String->Ordering testdata/Internals.lc 109:41-109:62 Ordering testdata/Internals.lc 109:59-109:60 V3 testdata/Internals.lc 109:61-109:62 V1 testdata/Internals.lc 110:13-110:17 Type testdata/Internals.lc 110:13-110:59 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 110:13-117:16 Type testdata/Internals.lc 110:13-120:29 V1 -> V2->Bool testdata/Internals.lc 110:33-110:37 Ordering->Bool testdata/Internals.lc 110:33-110:59 Bool testdata/Internals.lc 110:39-110:54 Char -> Char->Ordering testdata/Internals.lc 110:39-110:56 Char->Ordering testdata/Internals.lc 110:39-110:58 Ordering testdata/Internals.lc 110:55-110:56 V3 testdata/Internals.lc 110:57-110:58 V1 testdata/Internals.lc 111:13-111:16 Type testdata/Internals.lc 111:13-111:57 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 111:13-117:16 Type testdata/Internals.lc 111:13-120:29 V1 -> V2->Bool testdata/Internals.lc 111:32-111:36 Ordering->Bool testdata/Internals.lc 111:32-111:57 Bool testdata/Internals.lc 111:38-111:52 Int -> Int->Ordering testdata/Internals.lc 111:38-111:54 Int->Ordering testdata/Internals.lc 111:38-111:56 Ordering testdata/Internals.lc 111:53-111:54 V3 testdata/Internals.lc 111:55-111:56 V1 testdata/Internals.lc 112:13-112:18 Type testdata/Internals.lc 112:13-112:61 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 112:13-117:16 Type testdata/Internals.lc 112:13-120:29 V1 -> V2->Bool testdata/Internals.lc 112:34-112:38 Ordering->Bool testdata/Internals.lc 112:34-112:61 Bool testdata/Internals.lc 112:40-112:56 Float -> Float->Ordering testdata/Internals.lc 112:40-112:58 Float->Ordering testdata/Internals.lc 112:40-112:60 Ordering testdata/Internals.lc 112:57-112:58 V3 testdata/Internals.lc 112:59-112:60 V1 testdata/Internals.lc 113:13-113:17 Type testdata/Internals.lc 113:13-116:19 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 113:13-117:16 Type testdata/Internals.lc 113:13-120:29 V1 -> V2->Bool testdata/Internals.lc 114:5-114:9 V2 testdata/Internals.lc 114:5-116:19 Bool testdata/Internals.lc 114:13-114:17 Bool testdata/Internals.lc 114:13-116:19 Bool testdata/Internals.lc 114:20-114:24 Bool testdata/Internals.lc 114:20-116:19 Bool->Bool testdata/Internals.lc 115:14-115:19 V1 testdata/Internals.lc 115:14-116:19 Bool testdata/Internals.lc 115:22-115:26 Bool testdata/Internals.lc 115:22-116:19 Bool->Bool testdata/Internals.lc 116:14-116:19 Bool testdata/Internals.lc 117:13-117:16 Type testdata/Internals.lc 117:13-120:29 (V1 -> V2->Bool) -> V2 -> V3->Bool testdata/Internals.lc 118:5-118:9 V2 testdata/Internals.lc 118:5-120:29 Bool testdata/Internals.lc 118:15-118:19 V1 testdata/Internals.lc 118:15-120:29 Bool testdata/Internals.lc 118:24-118:28 Bool testdata/Internals.lc 118:24-120:29 Nat->Bool testdata/Internals.lc 119:15-119:19 Nat testdata/Internals.lc 119:15-120:29 Bool | Nat->Bool testdata/Internals.lc 119:24-119:25 Nat testdata/Internals.lc 119:24-119:28 Nat->Bool testdata/Internals.lc 119:24-119:30 Bool | Nat->Bool testdata/Internals.lc 119:24-120:29 Nat->Bool testdata/Internals.lc 119:26-119:28 {a} -> {b : Eq a} -> a -> a->Bool testdata/Internals.lc 119:29-119:30 Nat testdata/Internals.lc 120:24-120:29 Bool | Nat->Bool testdata/Internals.lc 122:6-122:10 Type | Type->Type testdata/Internals.lc 122:6-122:25 Type testdata/Internals.lc 122:6-122:36 Type testdata/Internals.lc 122:15-122:18 List V1 | {a} -> List a testdata/Internals.lc 122:21-122:25 List V4 | Type | {a} -> a -> List a -> List a testdata/Internals.lc 122:26-122:27 Type testdata/Internals.lc 122:29-122:33 Type->Type testdata/Internals.lc 122:29-122:35 Type testdata/Internals.lc 122:34-122:35 Type testdata/Internals.lc 126:6-126:11 List Type -> Type | Type testdata/Internals.lc 126:6-128:45 Type testdata/Internals.lc 126:16-126:20 Type testdata/Internals.lc 126:25-126:29 Type testdata/Internals.lc 127:5-127:9 () testdata/Internals.lc 127:5-127:22 Type testdata/Internals.lc 127:13-127:18 List Type -> Type testdata/Internals.lc 127:13-127:22 Type testdata/Internals.lc 127:19-127:22 {a} -> List a testdata/Internals.lc 128:5-128:10 HList ('Cons V3 V2) | {a} -> {b : List Type} -> a -> HList b -> HList ('Cons a b) testdata/Internals.lc 128:5-128:45 Type testdata/Internals.lc 128:14-128:15 V3 testdata/Internals.lc 128:14-128:45 Type testdata/Internals.lc 128:19-128:24 List Type -> Type testdata/Internals.lc 128:19-128:27 Type testdata/Internals.lc 128:19-128:45 Type testdata/Internals.lc 128:25-128:27 V2 testdata/Internals.lc 128:31-128:36 List Type -> Type testdata/Internals.lc 128:31-128:45 Type testdata/Internals.lc 128:39-128:40 Type testdata/Internals.lc 128:39-128:41 List Type -> List Type testdata/Internals.lc 128:39-128:44 List Type testdata/Internals.lc 128:40-128:41 {a} -> a -> List a -> List a testdata/Internals.lc 128:42-128:44 List Type testdata/Internals.lc 130:1-130:13 a:Type -> a -> ()->a testdata/Internals.lc 130:29-130:30 V1 testdata/Internals.lc 130:29-130:48 Type testdata/Internals.lc 130:34-130:39 List Type -> Type testdata/Internals.lc 130:34-130:43 Type testdata/Internals.lc 130:34-130:48 Type testdata/Internals.lc 130:40-130:43 {a} -> List a testdata/Internals.lc 130:47-130:48 Type testdata/Internals.lc 131:1-131:14 {a} -> {b : List Type} -> c:Type -> (a -> HList b -> c) -> HList ('Cons a b) -> c testdata/Internals.lc 132:21-132:25 Type testdata/Internals.lc 132:33-132:37 Type->Type testdata/Internals.lc 132:33-132:42 Type testdata/Internals.lc 132:33-136:9 Type testdata/Internals.lc 132:38-132:42 Type testdata/Internals.lc 133:8-136:9 Type testdata/Internals.lc 134:8-136:9 Type testdata/Internals.lc 134:9-134:10 Type testdata/Internals.lc 134:14-134:19 List Type -> Type testdata/Internals.lc 134:14-134:21 Type testdata/Internals.lc 134:14-134:26 Type testdata/Internals.lc 134:20-134:21 List Type testdata/Internals.lc 134:25-134:26 Type | V3 testdata/Internals.lc 135:8-135:13 List Type -> Type testdata/Internals.lc 135:8-135:24 Type testdata/Internals.lc 135:8-136:9 Type testdata/Internals.lc 135:15-135:19 {a} -> a -> List a -> List a testdata/Internals.lc 135:15-135:21 List Type -> List Type testdata/Internals.lc 135:15-135:23 List Type testdata/Internals.lc 135:20-135:21 Type testdata/Internals.lc 135:22-135:23 List Type testdata/Internals.lc 136:8-136:9 Type