summaryrefslogtreecommitdiff
path: root/testdata/Internals.out
diff options
context:
space:
mode:
authorPéter Diviánszky <divipp@gmail.com>2016-02-24 16:29:53 +0100
committerPéter Diviánszky <divipp@gmail.com>2016-02-24 16:31:12 +0100
commit82021fe9a4a7de991a16c7990ec9b41993e26df5 (patch)
treebbdb57c14630c512fe212a16371239cbfd21f51b /testdata/Internals.out
parent95e497050a191a68da9f170af13f0f10b01b7f91 (diff)
tweak namespace handling
Diffstat (limited to 'testdata/Internals.out')
-rw-r--r--testdata/Internals.out683
1 files changed, 334 insertions, 349 deletions
diff --git a/testdata/Internals.out b/testdata/Internals.out
index 2218a590..69645429 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -79,134 +79,138 @@ Cons :: {a} -> a -> 'List a -> 'List a
79'ListCase :: {a} -> (c : 'List a -> Type) -> c Nil -> (e:a -> (f : 'List a) -> c (Cons e f)) -> (h : 'List a) -> c h 79'ListCase :: {a} -> (c : 'List a -> Type) -> c Nil -> (e:a -> (f : 'List a) -> c (Cons e f)) -> (h : 'List a) -> c h
80match'List :: (b : Type->Type) -> (c:Type -> b ('List c)) -> e:Type -> b e -> b e 80match'List :: (b : Type->Type) -> (c:Type -> b ('List c)) -> e:Type -> b e -> b e
81'HList :: 'List Type -> Type 81'HList :: 'List Type -> Type
82HNil :: 'HList Nil 82HNil :: ()
83HCons :: {a} -> {b : 'List Type} -> a -> 'HList b -> 'HList (Cons a b) 83HCons :: {a} -> {b : 'List Type} -> a -> 'HList b -> 'HList (Cons a b)
84'HListCase :: (c : (a : 'List Type) -> 'HList a -> Type) -> c Nil HNil -> ({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 84'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
85match'HList :: (b : Type->Type) -> ((c : 'List Type) -> b ('HList c)) -> e:Type -> b e -> b e 85match'HList :: (b : Type->Type) -> ((c : 'List Type) -> b ('HList c)) -> e:Type -> b e -> b e
86hlistConsCase :: {a} -> {b : 'List Type} -> (d : 'Unit->Type) -> (a -> 'HList b -> d TT) -> 'HList (Cons a b) -> d TT 86hlistNilCase :: a:Type -> a -> ()->a
87hlistNilCase :: (b : 'Unit->Type) -> b TT -> 'HList Nil -> b TT 87hlistConsCase :: {a} -> {b : 'List Type} -> c:Type -> (a -> 'HList b -> c) -> 'HList (Cons a b) -> c
88joinTupleType :: {a} -> {b : 'List Type} -> a -> 'HList b -> 'HList (Cons a b)
89------------ tooltips 88------------ tooltips
90testdata/Internals.lc 7:1-7:8 {a} -> a->a 89testdata/Internals.lc 6:1-6:8 {a} -> a->a
91testdata/Internals.lc 7:13-7:14 V1 90testdata/Internals.lc 6:13-6:14 V1
92testdata/Internals.lc 10:1-10:7 {a} -> a->a 91testdata/Internals.lc 9:1-9:7 {a} -> a->a
93testdata/Internals.lc 10:12-10:13 V1 92testdata/Internals.lc 9:12-9:13 V1
94testdata/Internals.lc 12:1-12:10 {a}->a 93testdata/Internals.lc 11:1-11:10 {a}->a
95testdata/Internals.lc 12:27-12:31 Type 94testdata/Internals.lc 11:27-11:31 Type
96testdata/Internals.lc 12:35-12:36 Type 95testdata/Internals.lc 11:35-11:36 Type
97testdata/Internals.lc 14:1-14:8 {a} -> a->a -> a 96testdata/Internals.lc 13:1-13:8 {a} -> a->a -> a
98testdata/Internals.lc 14:25-14:29 Type 97testdata/Internals.lc 13:25-13:29 Type
99testdata/Internals.lc 14:33-14:46 Type 98testdata/Internals.lc 13:33-13:46 Type
100testdata/Internals.lc 14:34-14:35 Type 99testdata/Internals.lc 13:34-13:35 Type
101testdata/Internals.lc 14:39-14:40 Type 100testdata/Internals.lc 13:39-13:40 Type
102testdata/Internals.lc 14:45-14:46 Type 101testdata/Internals.lc 13:45-13:46 Type
103testdata/Internals.lc 16:6-16:10 Type 102testdata/Internals.lc 15:6-15:10 Type
104testdata/Internals.lc 16:6-16:15 Type 103testdata/Internals.lc 15:6-15:15 Type
105testdata/Internals.lc 16:13-16:15 Unit 104testdata/Internals.lc 15:13-15:15 Unit
106testdata/Internals.lc 17:6-17:12 Type 105testdata/Internals.lc 16:6-16:12 Type
107testdata/Internals.lc 18:6-18:11 String->Type | Type 106testdata/Internals.lc 17:6-17:11 String->Type | Type
108testdata/Internals.lc 18:18-18:24 Type 107testdata/Internals.lc 17:18-17:24 Type
109testdata/Internals.lc 20:1-20:13 {a} -> {b} -> a->b 108testdata/Internals.lc 19:1-19:13 {a} -> {b} -> a->b
110testdata/Internals.lc 20:30-20:31 V3 109testdata/Internals.lc 19:30-19:31 V3
111testdata/Internals.lc 20:30-20:36 Type 110testdata/Internals.lc 19:30-19:36 Type
112testdata/Internals.lc 20:35-20:36 Type | V2 111testdata/Internals.lc 19:35-19:36 Type | V2
113testdata/Internals.lc 23:13-23:17 a:Type -> a -> a->Type 112testdata/Internals.lc 22:13-22:17 a:Type -> a -> a->Type
114testdata/Internals.lc 23:24-23:28 Type 113testdata/Internals.lc 22:24-22:28 Type
115testdata/Internals.lc 23:36-23:37 Type 114testdata/Internals.lc 22:36-22:37 Type
116testdata/Internals.lc 23:36-23:46 Type 115testdata/Internals.lc 22:36-22:46 Type
117testdata/Internals.lc 23:45-23:46 Type 116testdata/Internals.lc 22:45-22:46 Type
118testdata/Internals.lc 32:1-32:8 a:Type -> a -> a->a 117testdata/Internals.lc 31:1-31:8 a:Type -> a -> a->a
119testdata/Internals.lc 32:24-32:25 V1 118testdata/Internals.lc 31:24-31:25 V1
120testdata/Internals.lc 32:24-32:35 Type 119testdata/Internals.lc 31:24-31:35 Type
121testdata/Internals.lc 32:29-32:30 Type 120testdata/Internals.lc 31:29-31:30 Type
122testdata/Internals.lc 32:29-32:35 Type 121testdata/Internals.lc 31:29-31:35 Type
123testdata/Internals.lc 32:34-32:35 Type 122testdata/Internals.lc 31:34-31:35 Type
124testdata/Internals.lc 35:13-35:15 Type -> Type->Type 123testdata/Internals.lc 34:13-34:15 Type -> Type->Type
125testdata/Internals.lc 37:1-37:11 (b : Type->Type) -> b Type -> d:Type -> b d -> b d 124testdata/Internals.lc 36:1-36:11 (b : Type->Type) -> b Type -> d:Type -> b d -> b d
126testdata/Internals.lc 37:28-37:32 Type 125testdata/Internals.lc 36:28-36:32 Type
127testdata/Internals.lc 37:36-37:40 Type 126testdata/Internals.lc 36:36-36:40 Type
128testdata/Internals.lc 37:45-37:46 Type->Type 127testdata/Internals.lc 36:45-36:46 Type->Type
129testdata/Internals.lc 37:45-37:51 Type 128testdata/Internals.lc 36:45-36:51 Type
130testdata/Internals.lc 37:45-37:87 Type 129testdata/Internals.lc 36:45-36:87 Type
131testdata/Internals.lc 37:47-37:51 Type 130testdata/Internals.lc 36:47-36:51 Type
132testdata/Internals.lc 37:55-37:87 Type 131testdata/Internals.lc 36:55-36:87 Type
133testdata/Internals.lc 37:68-37:72 Type 132testdata/Internals.lc 36:68-36:72 Type
134testdata/Internals.lc 37:77-37:78 Type->Type 133testdata/Internals.lc 36:77-36:78 Type->Type
135testdata/Internals.lc 37:77-37:80 Type 134testdata/Internals.lc 36:77-36:80 Type
136testdata/Internals.lc 37:77-37:87 Type 135testdata/Internals.lc 36:77-36:87 Type
137testdata/Internals.lc 37:79-37:80 Type 136testdata/Internals.lc 36:79-36:80 Type
138testdata/Internals.lc 37:84-37:85 Type->Type 137testdata/Internals.lc 36:84-36:85 Type->Type
139testdata/Internals.lc 37:84-37:87 Type 138testdata/Internals.lc 36:84-36:87 Type
140testdata/Internals.lc 37:86-37:87 Type 139testdata/Internals.lc 36:86-36:87 Type
141testdata/Internals.lc 39:6-39:11 {a} -> a -> a->Type 140testdata/Internals.lc 38:6-38:11 {a} -> a -> a->Type
142testdata/Internals.lc 39:14-39:18 a:Type -> a -> a->Type 141testdata/Internals.lc 38:14-38:18 a:Type -> a -> a->Type
143testdata/Internals.lc 39:14-39:20 V0 -> V1->Type 142testdata/Internals.lc 38:14-38:20 V0 -> V1->Type
144testdata/Internals.lc 42:1-42:4 Unit -> Unit->Unit 143testdata/Internals.lc 41:1-41:4 Unit -> Unit->Unit
145testdata/Internals.lc 42:8-42:12 Type 144testdata/Internals.lc 41:8-41:12 Type
146testdata/Internals.lc 42:16-42:20 Type 145testdata/Internals.lc 41:16-41:20 Type
147testdata/Internals.lc 42:16-42:28 Type 146testdata/Internals.lc 41:16-41:28 Type
148testdata/Internals.lc 42:24-42:28 Type 147testdata/Internals.lc 41:24-41:28 Type
149testdata/Internals.lc 45:6-45:9 Type 148testdata/Internals.lc 44:6-44:9 Type
150testdata/Internals.lc 46:6-46:10 Type 149testdata/Internals.lc 45:6-45:10 Type
151testdata/Internals.lc 47:6-47:11 Type 150testdata/Internals.lc 46:6-46:11 Type
152testdata/Internals.lc 48:6-48:10 Type 151testdata/Internals.lc 47:6-47:10 Type
153testdata/Internals.lc 50:6-50:10 Type 152testdata/Internals.lc 49:6-49:10 Type
154testdata/Internals.lc 50:6-50:25 Type 153testdata/Internals.lc 49:6-49:25 Type
155testdata/Internals.lc 50:13-50:18 Bool 154testdata/Internals.lc 49:13-49:18 Bool
156testdata/Internals.lc 50:21-50:25 Bool 155testdata/Internals.lc 49:21-49:25 Bool
157testdata/Internals.lc 52:6-52:14 Type 156testdata/Internals.lc 51:6-51:14 Type
158testdata/Internals.lc 52:6-52:29 Type 157testdata/Internals.lc 51:6-51:29 Type
159testdata/Internals.lc 52:17-52:19 Ordering 158testdata/Internals.lc 51:17-51:19 Ordering
160testdata/Internals.lc 52:22-52:24 Ordering 159testdata/Internals.lc 51:22-51:24 Ordering
161testdata/Internals.lc 52:27-52:29 Ordering 160testdata/Internals.lc 51:27-51:29 Ordering
162testdata/Internals.lc 54:6-54:9 Type 161testdata/Internals.lc 53:6-53:9 Type
163testdata/Internals.lc 54:6-54:23 Type 162testdata/Internals.lc 53:6-53:23 Type
164testdata/Internals.lc 54:12-54:16 Nat 163testdata/Internals.lc 53:12-53:16 Nat
165testdata/Internals.lc 54:19-54:23 Nat | Nat->Nat | Type 164testdata/Internals.lc 53:19-53:23 Nat | Nat->Nat | Type
166testdata/Internals.lc 54:24-54:27 Type 165testdata/Internals.lc 53:24-53:27 Type
167testdata/Internals.lc 57:1-57:14 Int->Word 166testdata/Internals.lc 56:1-56:14 Int->Word
167testdata/Internals.lc 56:24-56:27 Type
168testdata/Internals.lc 56:33-56:37 Type
169testdata/Internals.lc 57:1-57:15 Int->Float
168testdata/Internals.lc 57:24-57:27 Type 170testdata/Internals.lc 57:24-57:27 Type
169testdata/Internals.lc 57:33-57:37 Type 171testdata/Internals.lc 57:33-57:38 Type
170testdata/Internals.lc 58:1-58:15 Int->Float 172testdata/Internals.lc 58:1-58:13 Int->Nat
171testdata/Internals.lc 58:24-58:27 Type 173testdata/Internals.lc 58:24-58:27 Type
172testdata/Internals.lc 58:33-58:38 Type 174testdata/Internals.lc 58:33-58:36 Type
173testdata/Internals.lc 59:1-59:13 Int->Nat 175testdata/Internals.lc 59:1-59:15 Int -> Int->Ordering
174testdata/Internals.lc 59:24-59:27 Type 176testdata/Internals.lc 59:24-59:27 Type
175testdata/Internals.lc 59:33-59:36 Type 177testdata/Internals.lc 59:33-59:36 Type
176testdata/Internals.lc 60:1-60:15 Int -> Int->Ordering 178testdata/Internals.lc 59:33-59:50 Type
177testdata/Internals.lc 60:24-60:27 Type 179testdata/Internals.lc 59:42-59:50 Type
178testdata/Internals.lc 60:33-60:36 Type 180testdata/Internals.lc 60:1-60:16 Word -> Word->Ordering
181testdata/Internals.lc 60:24-60:28 Type
182testdata/Internals.lc 60:33-60:37 Type
179testdata/Internals.lc 60:33-60:50 Type 183testdata/Internals.lc 60:33-60:50 Type
180testdata/Internals.lc 60:42-60:50 Type 184testdata/Internals.lc 60:42-60:50 Type
181testdata/Internals.lc 61:1-61:16 Word -> Word->Ordering 185testdata/Internals.lc 61:1-61:17 Float -> Float->Ordering
182testdata/Internals.lc 61:24-61:28 Type 186testdata/Internals.lc 61:24-61:29 Type
183testdata/Internals.lc 61:33-61:37 Type 187testdata/Internals.lc 61:33-61:38 Type
184testdata/Internals.lc 61:33-61:50 Type 188testdata/Internals.lc 61:33-61:50 Type
185testdata/Internals.lc 61:42-61:50 Type 189testdata/Internals.lc 61:42-61:50 Type
186testdata/Internals.lc 62:1-62:17 Float -> Float->Ordering 190testdata/Internals.lc 62:1-62:16 Char -> Char->Ordering
187testdata/Internals.lc 62:24-62:29 Type 191testdata/Internals.lc 62:24-62:28 Type
188testdata/Internals.lc 62:33-62:38 Type 192testdata/Internals.lc 62:33-62:37 Type
189testdata/Internals.lc 62:33-62:50 Type 193testdata/Internals.lc 62:33-62:50 Type
190testdata/Internals.lc 62:42-62:50 Type 194testdata/Internals.lc 62:42-62:50 Type
191testdata/Internals.lc 63:1-63:16 Char -> Char->Ordering 195testdata/Internals.lc 63:1-63:18 String -> String->Ordering
192testdata/Internals.lc 63:24-63:28 Type 196testdata/Internals.lc 63:24-63:30 Type
193testdata/Internals.lc 63:33-63:37 Type 197testdata/Internals.lc 63:34-63:40 Type
194testdata/Internals.lc 63:33-63:50 Type 198testdata/Internals.lc 63:34-63:52 Type
195testdata/Internals.lc 63:42-63:50 Type 199testdata/Internals.lc 63:44-63:52 Type
196testdata/Internals.lc 64:1-64:18 String -> String->Ordering 200testdata/Internals.lc 64:1-64:14 Int->Int
197testdata/Internals.lc 64:24-64:30 Type 201testdata/Internals.lc 64:24-64:27 Type
198testdata/Internals.lc 64:34-64:40 Type 202testdata/Internals.lc 64:33-64:36 Type
199testdata/Internals.lc 64:34-64:52 Type 203testdata/Internals.lc 65:1-65:15 Word->Word
200testdata/Internals.lc 64:44-64:52 Type 204testdata/Internals.lc 65:24-65:28 Type
201testdata/Internals.lc 65:1-65:14 Int->Int 205testdata/Internals.lc 65:33-65:37 Type
202testdata/Internals.lc 65:24-65:27 Type 206testdata/Internals.lc 66:1-66:16 Float->Float
203testdata/Internals.lc 65:33-65:36 Type 207testdata/Internals.lc 66:24-66:29 Type
204testdata/Internals.lc 66:1-66:15 Word->Word 208testdata/Internals.lc 66:33-66:38 Type
205testdata/Internals.lc 66:24-66:28 Type 209testdata/Internals.lc 67:1-67:11 Int -> Int->Int
206testdata/Internals.lc 66:33-66:37 Type 210testdata/Internals.lc 67:24-67:27 Type
207testdata/Internals.lc 67:1-67:16 Float->Float 211testdata/Internals.lc 67:33-67:36 Type
208testdata/Internals.lc 67:24-67:29 Type 212testdata/Internals.lc 67:33-67:45 Type
209testdata/Internals.lc 67:33-67:38 Type 213testdata/Internals.lc 67:42-67:45 Type
210testdata/Internals.lc 68:1-68:11 Int -> Int->Int 214testdata/Internals.lc 68:1-68:11 Int -> Int->Int
211testdata/Internals.lc 68:24-68:27 Type 215testdata/Internals.lc 68:24-68:27 Type
212testdata/Internals.lc 68:33-68:36 Type 216testdata/Internals.lc 68:33-68:36 Type
@@ -217,254 +221,235 @@ testdata/Internals.lc 69:24-69:27 Type
217testdata/Internals.lc 69:33-69:36 Type 221testdata/Internals.lc 69:33-69:36 Type
218testdata/Internals.lc 69:33-69:45 Type 222testdata/Internals.lc 69:33-69:45 Type
219testdata/Internals.lc 69:42-69:45 Type 223testdata/Internals.lc 69:42-69:45 Type
220testdata/Internals.lc 70:1-70:11 Int -> Int->Int 224testdata/Internals.lc 70:1-70:14 Float->Float
221testdata/Internals.lc 70:24-70:27 Type 225testdata/Internals.lc 70:24-70:29 Type
222testdata/Internals.lc 70:33-70:36 Type 226testdata/Internals.lc 70:33-70:38 Type
223testdata/Internals.lc 70:33-70:45 Type 227testdata/Internals.lc 71:1-71:10 Float->Int
224testdata/Internals.lc 70:42-70:45 Type
225testdata/Internals.lc 71:1-71:14 Float->Float
226testdata/Internals.lc 71:24-71:29 Type 228testdata/Internals.lc 71:24-71:29 Type
227testdata/Internals.lc 71:33-71:38 Type 229testdata/Internals.lc 71:33-71:36 Type
228testdata/Internals.lc 72:1-72:10 Float->Int 230testdata/Internals.lc 74:19-74:23 Type
229testdata/Internals.lc 72:24-72:29 Type 231testdata/Internals.lc 74:19-74:38 Type
230testdata/Internals.lc 72:33-72:36 Type 232testdata/Internals.lc 74:27-74:28 V2
231testdata/Internals.lc 75:19-75:23 Type 233testdata/Internals.lc 74:27-74:38 Type
232testdata/Internals.lc 75:19-75:38 Type 234testdata/Internals.lc 74:32-74:33 Type
233testdata/Internals.lc 75:27-75:28 V2 235testdata/Internals.lc 74:32-74:38 Type
234testdata/Internals.lc 75:27-75:38 Type 236testdata/Internals.lc 74:37-74:38 Type
235testdata/Internals.lc 75:32-75:33 Type 237testdata/Internals.lc 75:1-75:15 {a} -> Bool -> a -> a->a
236testdata/Internals.lc 75:32-75:38 Type 238testdata/Internals.lc 75:16-75:20 Bool
237testdata/Internals.lc 75:37-75:38 Type 239testdata/Internals.lc 75:16-76:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
238testdata/Internals.lc 76:1-76:15 {a} -> Bool -> a -> a->a 240testdata/Internals.lc 75:28-75:29 V3
239testdata/Internals.lc 76:16-76:20 Bool 241testdata/Internals.lc 75:28-76:29 Bool->V4
240testdata/Internals.lc 76:16-77:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3 242testdata/Internals.lc 76:28-76:29 V4
241testdata/Internals.lc 76:28-76:29 V3 243testdata/Internals.lc 78:1-78:5 Ordering->Bool
242testdata/Internals.lc 76:28-77:29 Bool->V4 244testdata/Internals.lc 78:6-78:8 V1
243testdata/Internals.lc 77:28-77:29 V4 245testdata/Internals.lc 78:6-79:15 Bool
244testdata/Internals.lc 79:1-79:5 Ordering->Bool 246testdata/Internals.lc 78:11-78:15 Bool
245testdata/Internals.lc 79:6-79:8 V1 247testdata/Internals.lc 78:11-79:15 Bool -> Ordering->Bool
246testdata/Internals.lc 79:6-80:15 Bool 248testdata/Internals.lc 79:10-79:15 Bool
247testdata/Internals.lc 79:11-79:15 Bool 249testdata/Internals.lc 82:7-82:10 Type->Type
248testdata/Internals.lc 79:11-80:15 Bool -> Ordering->Bool 250testdata/Internals.lc 82:7-83:22 Type
249testdata/Internals.lc 80:10-80:15 Bool 251testdata/Internals.lc 82:7-84:32 Type
250testdata/Internals.lc 83:7-83:10 Type->Type 252testdata/Internals.lc 82:7-85:19 Type
251testdata/Internals.lc 83:7-84:22 Type 253testdata/Internals.lc 83:3-83:10 {a} -> {b : Num a} -> Int->a
252testdata/Internals.lc 83:7-85:32 Type 254testdata/Internals.lc 83:14-83:17 Type
253testdata/Internals.lc 83:7-86:19 Type 255testdata/Internals.lc 83:14-83:22 Type
254testdata/Internals.lc 84:3-84:10 {a} -> {b : Num a} -> Int->a 256testdata/Internals.lc 83:21-83:22 Type
255testdata/Internals.lc 84:14-84:17 Type 257testdata/Internals.lc 84:3-84:10 {a} -> {b : Num a} -> a -> a->Ordering
256testdata/Internals.lc 84:14-84:22 Type 258testdata/Internals.lc 84:14-84:15 Type
257testdata/Internals.lc 84:21-84:22 Type 259testdata/Internals.lc 84:14-84:32 Type
258testdata/Internals.lc 85:3-85:10 {a} -> {b : Num a} -> a -> a->Ordering 260testdata/Internals.lc 84:19-84:20 Type
259testdata/Internals.lc 85:14-85:15 Type 261testdata/Internals.lc 84:19-84:32 Type
260testdata/Internals.lc 85:14-85:32 Type 262testdata/Internals.lc 84:24-84:32 Type
261testdata/Internals.lc 85:19-85:20 Type 263testdata/Internals.lc 85:3-85:9 {a} -> {b : Num a} -> a->a
262testdata/Internals.lc 85:19-85:32 Type 264testdata/Internals.lc 85:13-85:14 Type
263testdata/Internals.lc 85:24-85:32 Type 265testdata/Internals.lc 85:13-85:19 Type
264testdata/Internals.lc 86:3-86:9 {a} -> {b : Num a} -> a->a 266testdata/Internals.lc 85:18-85:19 Type
265testdata/Internals.lc 86:13-86:14 Type 267testdata/Internals.lc 87:14-87:17 Type
266testdata/Internals.lc 86:13-86:19 Type 268testdata/Internals.lc 87:14-88:20 Int->V2 -> Int->V3
267testdata/Internals.lc 86:18-86:19 Type 269testdata/Internals.lc 87:14-89:27 (V1 -> V2->Ordering) -> V2 -> V3->Ordering
268testdata/Internals.lc 88:14-88:17 Type 270testdata/Internals.lc 87:14-90:26 V1->V2 -> V2->V3
269testdata/Internals.lc 88:14-89:20 Int->V2 -> Int->V3 271testdata/Internals.lc 87:14-99:17 Type | Type->Type
270testdata/Internals.lc 88:14-90:27 (V1 -> V2->Ordering) -> V2 -> V3->Ordering 272testdata/Internals.lc 87:14-100:25 Int->V2 | {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
271testdata/Internals.lc 88:14-91:26 V1->V2 -> V2->V3 273testdata/Internals.lc 87:14-101:22 V1 -> V2->Ordering | {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
272testdata/Internals.lc 88:14-100:17 Type | Type->Type 274testdata/Internals.lc 87:14-102:22 V1->V2 | {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
273testdata/Internals.lc 88:14-101:25 Int->V2 | {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a 275testdata/Internals.lc 88:19-88:20 V1
274testdata/Internals.lc 88:14-102:22 V1 -> V2->Ordering | {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering 276testdata/Internals.lc 89:13-89:27 Int -> Int->Ordering
275testdata/Internals.lc 88:14-103:22 V1->V2 | {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a 277testdata/Internals.lc 90:13-90:26 Int->Int
276testdata/Internals.lc 89:19-89:20 V1 278testdata/Internals.lc 91:14-91:18 Type
277testdata/Internals.lc 90:13-90:27 Int -> Int->Ordering 279testdata/Internals.lc 91:14-92:26 Int->V2 -> Int->V3
278testdata/Internals.lc 91:13-91:26 Int->Int 280testdata/Internals.lc 91:14-93:28 (V1 -> V2->Ordering) -> V2 -> V3->Ordering
279testdata/Internals.lc 92:14-92:18 Type 281testdata/Internals.lc 91:14-94:27 V1->V2 -> V2->V3
280testdata/Internals.lc 92:14-93:26 Int->V2 -> Int->V3 282testdata/Internals.lc 91:14-99:17 Type
281testdata/Internals.lc 92:14-94:28 (V1 -> V2->Ordering) -> V2 -> V3->Ordering 283testdata/Internals.lc 91:14-100:25 Int->V2
282testdata/Internals.lc 92:14-95:27 V1->V2 -> V2->V3 284testdata/Internals.lc 91:14-101:22 V1 -> V2->Ordering
283testdata/Internals.lc 92:14-100:17 Type 285testdata/Internals.lc 91:14-102:22 V1->V2
284testdata/Internals.lc 92:14-101:25 Int->V2 286testdata/Internals.lc 92:13-92:26 Int->Word
285testdata/Internals.lc 92:14-102:22 V1 -> V2->Ordering 287testdata/Internals.lc 93:13-93:28 Word -> Word->Ordering
286testdata/Internals.lc 92:14-103:22 V1->V2 288testdata/Internals.lc 94:13-94:27 Word->Word
287testdata/Internals.lc 93:13-93:26 Int->Word 289testdata/Internals.lc 95:14-95:19 Type
288testdata/Internals.lc 94:13-94:28 Word -> Word->Ordering 290testdata/Internals.lc 95:14-96:27 Int->V2 -> Int->V3
289testdata/Internals.lc 95:13-95:27 Word->Word 291testdata/Internals.lc 95:14-97:29 (V1 -> V2->Ordering) -> V2 -> V3->Ordering
290testdata/Internals.lc 96:14-96:19 Type 292testdata/Internals.lc 95:14-98:28 V1->V2 -> V2->V3
291testdata/Internals.lc 96:14-97:27 Int->V2 -> Int->V3 293testdata/Internals.lc 95:14-99:17 Type
292testdata/Internals.lc 96:14-98:29 (V1 -> V2->Ordering) -> V2 -> V3->Ordering 294testdata/Internals.lc 95:14-100:25 Int->V2
293testdata/Internals.lc 96:14-99:28 V1->V2 -> V2->V3 295testdata/Internals.lc 95:14-101:22 V1 -> V2->Ordering
294testdata/Internals.lc 96:14-100:17 Type 296testdata/Internals.lc 95:14-102:22 V1->V2
295testdata/Internals.lc 96:14-101:25 Int->V2 297testdata/Internals.lc 96:13-96:27 Int->Float
296testdata/Internals.lc 96:14-102:22 V1 -> V2->Ordering 298testdata/Internals.lc 97:13-97:29 Float -> Float->Ordering
297testdata/Internals.lc 96:14-103:22 V1->V2 299testdata/Internals.lc 98:13-98:28 Float->Float
298testdata/Internals.lc 97:13-97:27 Int->Float 300testdata/Internals.lc 99:14-99:17 Type
299testdata/Internals.lc 98:13-98:29 Float -> Float->Ordering 301testdata/Internals.lc 99:14-100:25 Int->V2 -> Int->V3
300testdata/Internals.lc 99:13-99:28 Float->Float 302testdata/Internals.lc 99:14-101:22 (V1 -> V2->Ordering) -> V2 -> V3->Ordering
301testdata/Internals.lc 100:14-100:17 Type 303testdata/Internals.lc 99:14-102:22 V1->V2 -> V2->V3
302testdata/Internals.lc 100:14-101:25 Int->V2 -> Int->V3 304testdata/Internals.lc 100:13-100:25 Int->Nat
303testdata/Internals.lc 100:14-102:22 (V1 -> V2->Ordering) -> V2 -> V3->Ordering 305testdata/Internals.lc 101:13-101:22 {a}->a
304testdata/Internals.lc 100:14-103:22 V1->V2 -> V2->V3
305testdata/Internals.lc 101:13-101:25 Int->Nat
306testdata/Internals.lc 102:13-102:22 {a}->a 306testdata/Internals.lc 102:13-102:22 {a}->a
307testdata/Internals.lc 103:13-103:22 {a}->a 307testdata/Internals.lc 104:7-104:9 Type->Type
308testdata/Internals.lc 105:7-105:9 Type->Type 308testdata/Internals.lc 104:7-105:27 Type
309testdata/Internals.lc 105:7-106:27 Type 309testdata/Internals.lc 104:7-120:29 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool
310testdata/Internals.lc 105:7-121:29 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool 310testdata/Internals.lc 105:6-105:8 {a} -> {b : Eq a} -> a -> a->Bool
311testdata/Internals.lc 106:6-106:8 {a} -> {b : Eq a} -> a -> a->Bool 311testdata/Internals.lc 105:13-105:14 Type
312testdata/Internals.lc 106:13-106:14 Type 312testdata/Internals.lc 105:13-105:27 Type
313testdata/Internals.lc 106:13-106:27 Type 313testdata/Internals.lc 105:18-105:19 Type
314testdata/Internals.lc 106:18-106:19 Type 314testdata/Internals.lc 105:18-105:27 Type
315testdata/Internals.lc 106:18-106:27 Type 315testdata/Internals.lc 105:23-105:27 Type
316testdata/Internals.lc 106:23-106:27 Type 316testdata/Internals.lc 109:13-109:19 Type
317testdata/Internals.lc 110:13-110:19 Type 317testdata/Internals.lc 109:13-109:63 (V1 -> V2->Bool) -> V2 -> V3->Bool
318testdata/Internals.lc 110:13-110:63 (V1 -> V2->Bool) -> V2 -> V3->Bool 318testdata/Internals.lc 109:13-117:16 Type | Type->Type
319testdata/Internals.lc 110:13-118:16 Type | Type->Type 319testdata/Internals.lc 109:13-120:29 V1 -> V2->Bool | {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
320testdata/Internals.lc 110:13-121:29 V1 -> V2->Bool | {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool 320testdata/Internals.lc 109:35-109:39 Ordering->Bool
321testdata/Internals.lc 110:35-110:39 Ordering->Bool 321testdata/Internals.lc 109:35-109:63 Bool
322testdata/Internals.lc 110:35-110:63 Bool 322testdata/Internals.lc 109:41-109:58 String -> String->Ordering
323testdata/Internals.lc 110:41-110:58 String -> String->Ordering 323testdata/Internals.lc 109:41-109:60 String->Ordering
324testdata/Internals.lc 110:41-110:60 String->Ordering 324testdata/Internals.lc 109:41-109:62 Ordering
325testdata/Internals.lc 110:41-110:62 Ordering 325testdata/Internals.lc 109:59-109:60 V3
326testdata/Internals.lc 110:59-110:60 V3 326testdata/Internals.lc 109:61-109:62 V1
327testdata/Internals.lc 110:61-110:62 V1 327testdata/Internals.lc 110:13-110:17 Type
328testdata/Internals.lc 111:13-111:17 Type 328testdata/Internals.lc 110:13-110:59 (V1 -> V2->Bool) -> V2 -> V3->Bool
329testdata/Internals.lc 111:13-111:59 (V1 -> V2->Bool) -> V2 -> V3->Bool 329testdata/Internals.lc 110:13-117:16 Type
330testdata/Internals.lc 111:13-118:16 Type 330testdata/Internals.lc 110:13-120:29 V1 -> V2->Bool
331testdata/Internals.lc 111:13-121:29 V1 -> V2->Bool 331testdata/Internals.lc 110:33-110:37 Ordering->Bool
332testdata/Internals.lc 111:33-111:37 Ordering->Bool 332testdata/Internals.lc 110:33-110:59 Bool
333testdata/Internals.lc 111:33-111:59 Bool 333testdata/Internals.lc 110:39-110:54 Char -> Char->Ordering
334testdata/Internals.lc 111:39-111:54 Char -> Char->Ordering 334testdata/Internals.lc 110:39-110:56 Char->Ordering
335testdata/Internals.lc 111:39-111:56 Char->Ordering 335testdata/Internals.lc 110:39-110:58 Ordering
336testdata/Internals.lc 111:39-111:58 Ordering 336testdata/Internals.lc 110:55-110:56 V3
337testdata/Internals.lc 111:55-111:56 V3 337testdata/Internals.lc 110:57-110:58 V1
338testdata/Internals.lc 111:57-111:58 V1 338testdata/Internals.lc 111:13-111:16 Type
339testdata/Internals.lc 112:13-112:16 Type 339testdata/Internals.lc 111:13-111:57 (V1 -> V2->Bool) -> V2 -> V3->Bool
340testdata/Internals.lc 112:13-112:57 (V1 -> V2->Bool) -> V2 -> V3->Bool 340testdata/Internals.lc 111:13-117:16 Type
341testdata/Internals.lc 112:13-118:16 Type 341testdata/Internals.lc 111:13-120:29 V1 -> V2->Bool
342testdata/Internals.lc 112:13-121:29 V1 -> V2->Bool 342testdata/Internals.lc 111:32-111:36 Ordering->Bool
343testdata/Internals.lc 112:32-112:36 Ordering->Bool 343testdata/Internals.lc 111:32-111:57 Bool
344testdata/Internals.lc 112:32-112:57 Bool 344testdata/Internals.lc 111:38-111:52 Int -> Int->Ordering
345testdata/Internals.lc 112:38-112:52 Int -> Int->Ordering 345testdata/Internals.lc 111:38-111:54 Int->Ordering
346testdata/Internals.lc 112:38-112:54 Int->Ordering 346testdata/Internals.lc 111:38-111:56 Ordering
347testdata/Internals.lc 112:38-112:56 Ordering 347testdata/Internals.lc 111:53-111:54 V3
348testdata/Internals.lc 112:53-112:54 V3 348testdata/Internals.lc 111:55-111:56 V1
349testdata/Internals.lc 112:55-112:56 V1 349testdata/Internals.lc 112:13-112:18 Type
350testdata/Internals.lc 113:13-113:18 Type 350testdata/Internals.lc 112:13-112:61 (V1 -> V2->Bool) -> V2 -> V3->Bool
351testdata/Internals.lc 113:13-113:61 (V1 -> V2->Bool) -> V2 -> V3->Bool 351testdata/Internals.lc 112:13-117:16 Type
352testdata/Internals.lc 113:13-118:16 Type 352testdata/Internals.lc 112:13-120:29 V1 -> V2->Bool
353testdata/Internals.lc 113:13-121:29 V1 -> V2->Bool 353testdata/Internals.lc 112:34-112:38 Ordering->Bool
354testdata/Internals.lc 113:34-113:38 Ordering->Bool 354testdata/Internals.lc 112:34-112:61 Bool
355testdata/Internals.lc 113:34-113:61 Bool 355testdata/Internals.lc 112:40-112:56 Float -> Float->Ordering
356testdata/Internals.lc 113:40-113:56 Float -> Float->Ordering 356testdata/Internals.lc 112:40-112:58 Float->Ordering
357testdata/Internals.lc 113:40-113:58 Float->Ordering 357testdata/Internals.lc 112:40-112:60 Ordering
358testdata/Internals.lc 113:40-113:60 Ordering 358testdata/Internals.lc 112:57-112:58 V3
359testdata/Internals.lc 113:57-113:58 V3 359testdata/Internals.lc 112:59-112:60 V1
360testdata/Internals.lc 113:59-113:60 V1 360testdata/Internals.lc 113:13-113:17 Type
361testdata/Internals.lc 114:13-114:17 Type 361testdata/Internals.lc 113:13-116:19 (V1 -> V2->Bool) -> V2 -> V3->Bool
362testdata/Internals.lc 114:13-117:19 (V1 -> V2->Bool) -> V2 -> V3->Bool 362testdata/Internals.lc 113:13-117:16 Type
363testdata/Internals.lc 114:13-118:16 Type 363testdata/Internals.lc 113:13-120:29 V1 -> V2->Bool
364testdata/Internals.lc 114:13-121:29 V1 -> V2->Bool 364testdata/Internals.lc 114:5-114:9 V2
365testdata/Internals.lc 115:5-115:9 V2 365testdata/Internals.lc 114:5-116:19 Bool
366testdata/Internals.lc 115:5-117:19 Bool 366testdata/Internals.lc 114:13-114:17 Bool
367testdata/Internals.lc 115:13-115:17 Bool 367testdata/Internals.lc 114:13-116:19 Bool
368testdata/Internals.lc 115:13-117:19 Bool 368testdata/Internals.lc 114:20-114:24 Bool
369testdata/Internals.lc 115:20-115:24 Bool 369testdata/Internals.lc 114:20-116:19 Bool->Bool
370testdata/Internals.lc 115:20-117:19 Bool->Bool 370testdata/Internals.lc 115:14-115:19 V1
371testdata/Internals.lc 116:14-116:19 V1 371testdata/Internals.lc 115:14-116:19 Bool
372testdata/Internals.lc 116:14-117:19 Bool 372testdata/Internals.lc 115:22-115:26 Bool
373testdata/Internals.lc 116:22-116:26 Bool 373testdata/Internals.lc 115:22-116:19 Bool->Bool
374testdata/Internals.lc 116:22-117:19 Bool->Bool 374testdata/Internals.lc 116:14-116:19 Bool
375testdata/Internals.lc 117:14-117:19 Bool 375testdata/Internals.lc 117:13-117:16 Type
376testdata/Internals.lc 118:13-118:16 Type 376testdata/Internals.lc 117:13-120:29 (V1 -> V2->Bool) -> V2 -> V3->Bool
377testdata/Internals.lc 118:13-121:29 (V1 -> V2->Bool) -> V2 -> V3->Bool 377testdata/Internals.lc 118:5-118:9 V2
378testdata/Internals.lc 119:5-119:9 V2 378testdata/Internals.lc 118:5-120:29 Bool
379testdata/Internals.lc 119:5-121:29 Bool 379testdata/Internals.lc 118:15-118:19 V1
380testdata/Internals.lc 119:15-119:19 V1 380testdata/Internals.lc 118:15-120:29 Bool
381testdata/Internals.lc 119:15-121:29 Bool 381testdata/Internals.lc 118:24-118:28 Bool
382testdata/Internals.lc 119:24-119:28 Bool 382testdata/Internals.lc 118:24-120:29 Nat->Bool
383testdata/Internals.lc 119:24-121:29 Nat->Bool 383testdata/Internals.lc 119:15-119:19 Nat
384testdata/Internals.lc 120:15-120:19 Nat 384testdata/Internals.lc 119:15-120:29 Bool | Nat->Bool
385testdata/Internals.lc 120:15-121:29 Bool | Nat->Bool 385testdata/Internals.lc 119:24-119:25 Nat
386testdata/Internals.lc 120:24-120:25 Nat 386testdata/Internals.lc 119:24-119:28 Nat->Bool
387testdata/Internals.lc 120:24-120:28 Nat->Bool 387testdata/Internals.lc 119:24-119:30 Bool | Nat->Bool
388testdata/Internals.lc 120:24-120:30 Bool | Nat->Bool 388testdata/Internals.lc 119:24-120:29 Nat->Bool
389testdata/Internals.lc 120:24-121:29 Nat->Bool 389testdata/Internals.lc 119:26-119:28 {a} -> {b : Eq a} -> a -> a->Bool
390testdata/Internals.lc 120:26-120:28 {a} -> {b : Eq a} -> a -> a->Bool 390testdata/Internals.lc 119:29-119:30 Nat
391testdata/Internals.lc 120:29-120:30 Nat 391testdata/Internals.lc 120:24-120:29 Bool | Nat->Bool
392testdata/Internals.lc 121:24-121:29 Bool | Nat->Bool 392testdata/Internals.lc 122:6-122:10 Type | Type->Type
393testdata/Internals.lc 123:6-123:10 Type | Type->Type 393testdata/Internals.lc 122:6-122:25 Type
394testdata/Internals.lc 123:6-123:25 Type 394testdata/Internals.lc 122:6-122:36 Type
395testdata/Internals.lc 123:6-123:36 Type 395testdata/Internals.lc 122:15-122:18 List V1 | {a} -> List a
396testdata/Internals.lc 123:15-123:18 List V1 | {a} -> List a 396testdata/Internals.lc 122:21-122:25 List V4 | Type | {a} -> a -> List a -> List a
397testdata/Internals.lc 123:21-123:25 List V4 | Type | {a} -> a -> List a -> List a 397testdata/Internals.lc 122:26-122:27 Type
398testdata/Internals.lc 123:26-123:27 Type 398testdata/Internals.lc 122:29-122:33 Type->Type
399testdata/Internals.lc 123:29-123:33 Type->Type 399testdata/Internals.lc 122:29-122:35 Type
400testdata/Internals.lc 123:29-123:35 Type 400testdata/Internals.lc 122:34-122:35 Type
401testdata/Internals.lc 123:34-123:35 Type 401testdata/Internals.lc 126:6-126:11 List Type -> Type | Type
402testdata/Internals.lc 127:6-127:11 List Type -> Type | Type 402testdata/Internals.lc 126:6-128:45 Type
403testdata/Internals.lc 127:6-129:45 Type 403testdata/Internals.lc 126:16-126:20 Type
404testdata/Internals.lc 127:16-127:20 Type 404testdata/Internals.lc 126:25-126:29 Type
405testdata/Internals.lc 127:25-127:29 Type 405testdata/Internals.lc 127:5-127:9 ()
406testdata/Internals.lc 128:5-128:9 HList 'Nil 406testdata/Internals.lc 127:5-127:22 Type
407testdata/Internals.lc 128:5-128:22 Type 407testdata/Internals.lc 127:13-127:18 List Type -> Type
408testdata/Internals.lc 128:13-128:18 List Type -> Type 408testdata/Internals.lc 127:13-127:22 Type
409testdata/Internals.lc 128:13-128:22 Type 409testdata/Internals.lc 127:19-127:22 {a} -> List a
410testdata/Internals.lc 128:19-128:22 {a} -> List a 410testdata/Internals.lc 128:5-128:10 HList ('Cons V3 V2) | {a} -> {b : List Type} -> a -> HList b -> HList ('Cons a b)
411testdata/Internals.lc 129:5-129:10 HList ('Cons V3 V2) | {a} -> {b : List Type} -> a -> HList b -> HList ('Cons a b) 411testdata/Internals.lc 128:5-128:45 Type
412testdata/Internals.lc 129:5-129:45 Type 412testdata/Internals.lc 128:14-128:15 V3
413testdata/Internals.lc 129:14-129:15 V3 413testdata/Internals.lc 128:14-128:45 Type
414testdata/Internals.lc 129:14-129:45 Type 414testdata/Internals.lc 128:19-128:24 List Type -> Type
415testdata/Internals.lc 129:19-129:24 List Type -> Type 415testdata/Internals.lc 128:19-128:27 Type
416testdata/Internals.lc 129:19-129:27 Type 416testdata/Internals.lc 128:19-128:45 Type
417testdata/Internals.lc 129:19-129:45 Type 417testdata/Internals.lc 128:25-128:27 V2
418testdata/Internals.lc 129:25-129:27 V2 418testdata/Internals.lc 128:31-128:36 List Type -> Type
419testdata/Internals.lc 129:31-129:36 List Type -> Type 419testdata/Internals.lc 128:31-128:45 Type
420testdata/Internals.lc 129:31-129:45 Type 420testdata/Internals.lc 128:39-128:40 Type
421testdata/Internals.lc 129:39-129:40 Type 421testdata/Internals.lc 128:39-128:41 List Type -> List Type
422testdata/Internals.lc 129:39-129:41 List Type -> List Type 422testdata/Internals.lc 128:39-128:44 List Type
423testdata/Internals.lc 129:39-129:44 List Type 423testdata/Internals.lc 128:40-128:41 {a} -> a -> List a -> List a
424testdata/Internals.lc 129:40-129:41 {a} -> a -> List a -> List a 424testdata/Internals.lc 128:42-128:44 List Type
425testdata/Internals.lc 129:42-129:44 List Type 425testdata/Internals.lc 130:1-130:13 a:Type -> a -> ()->a
426testdata/Internals.lc 131:1-131:14 {a} -> {b : List Type} -> (d : Unit->Type) -> (a -> HList b -> d 'TT) -> HList ('Cons a b) -> d 'TT 426testdata/Internals.lc 130:29-130:30 V1
427testdata/Internals.lc 130:29-130:48 Type
428testdata/Internals.lc 130:34-130:39 List Type -> Type
429testdata/Internals.lc 130:34-130:43 Type
430testdata/Internals.lc 130:34-130:48 Type
431testdata/Internals.lc 130:40-130:43 {a} -> List a
432testdata/Internals.lc 130:47-130:48 Type
433testdata/Internals.lc 131:1-131:14 {a} -> {b : List Type} -> c:Type -> (a -> HList b -> c) -> HList ('Cons a b) -> c
427testdata/Internals.lc 132:21-132:25 Type 434testdata/Internals.lc 132:21-132:25 Type
428testdata/Internals.lc 132:33-132:37 Type->Type 435testdata/Internals.lc 132:33-132:37 Type->Type
429testdata/Internals.lc 132:33-132:42 Type 436testdata/Internals.lc 132:33-132:42 Type
430testdata/Internals.lc 132:33-136:13 Type 437testdata/Internals.lc 132:33-136:9 Type
431testdata/Internals.lc 132:38-132:42 Type 438testdata/Internals.lc 132:38-132:42 Type
432testdata/Internals.lc 133:8-136:13 Type 439testdata/Internals.lc 133:8-136:9 Type
433testdata/Internals.lc 133:21-133:25 Type 440testdata/Internals.lc 134:8-136:9 Type
434testdata/Internals.lc 133:29-133:33 Type
435testdata/Internals.lc 134:8-136:13 Type
436testdata/Internals.lc 134:9-134:10 Type 441testdata/Internals.lc 134:9-134:10 Type
437testdata/Internals.lc 134:14-134:19 List Type -> Type 442testdata/Internals.lc 134:14-134:19 List Type -> Type
438testdata/Internals.lc 134:14-134:21 Type 443testdata/Internals.lc 134:14-134:21 Type
439testdata/Internals.lc 134:14-134:30 Type 444testdata/Internals.lc 134:14-134:26 Type
440testdata/Internals.lc 134:20-134:21 List Type 445testdata/Internals.lc 134:20-134:21 List Type
441testdata/Internals.lc 134:25-134:26 Unit->Type 446testdata/Internals.lc 134:25-134:26 Type | V3
442testdata/Internals.lc 134:25-134:30 Type
443testdata/Internals.lc 134:27-134:30 Unit
444testdata/Internals.lc 135:8-135:13 List Type -> Type 447testdata/Internals.lc 135:8-135:13 List Type -> Type
445testdata/Internals.lc 135:8-135:24 Type 448testdata/Internals.lc 135:8-135:24 Type
446testdata/Internals.lc 135:8-136:13 Type 449testdata/Internals.lc 135:8-136:9 Type
447testdata/Internals.lc 135:15-135:19 {a} -> a -> List a -> List a 450testdata/Internals.lc 135:15-135:19 {a} -> a -> List a -> List a
448testdata/Internals.lc 135:15-135:21 List Type -> List Type 451testdata/Internals.lc 135:15-135:21 List Type -> List Type
449testdata/Internals.lc 135:15-135:23 List Type 452testdata/Internals.lc 135:15-135:23 List Type
450testdata/Internals.lc 135:20-135:21 Type 453testdata/Internals.lc 135:20-135:21 Type
451testdata/Internals.lc 135:22-135:23 List Type 454testdata/Internals.lc 135:22-135:23 List Type
452testdata/Internals.lc 136:8-136:9 Unit->Type 455testdata/Internals.lc 136:8-136:9 Type
453testdata/Internals.lc 136:8-136:13 Type
454testdata/Internals.lc 136:10-136:13 Unit
455testdata/Internals.lc 145:1-145:13 (b : Unit->Type) -> b 'TT -> HList 'Nil -> b 'TT
456testdata/Internals.lc 145:30-145:34 Type
457testdata/Internals.lc 145:38-145:42 Type
458testdata/Internals.lc 145:47-145:48 Unit->Type
459testdata/Internals.lc 145:47-145:52 Type
460testdata/Internals.lc 145:47-145:74 Type
461testdata/Internals.lc 145:49-145:52 Unit
462testdata/Internals.lc 145:56-145:61 List Type -> Type
463testdata/Internals.lc 145:56-145:65 Type
464testdata/Internals.lc 145:56-145:74 Type
465testdata/Internals.lc 145:62-145:65 {a} -> List a
466testdata/Internals.lc 145:69-145:70 Unit->Type
467testdata/Internals.lc 145:69-145:74 Type
468testdata/Internals.lc 145:71-145:74 Unit
469testdata/Internals.lc 171:1-171:14 {a} -> {b : List Type} -> a -> HList b -> HList ('Cons a b)
470testdata/Internals.lc 171:17-171:22 {a} -> {b : List Type} -> a -> HList b -> HList ('Cons a b)