diff options
Diffstat (limited to 'testdata')
-rw-r--r-- | testdata/Builtins.out | 1815 |
1 files changed, 914 insertions, 901 deletions
diff --git a/testdata/Builtins.out b/testdata/Builtins.out index 2add020d..877414f4 100644 --- a/testdata/Builtins.out +++ b/testdata/Builtins.out | |||
@@ -1166,936 +1166,949 @@ testdata/Builtins.lc 356:15-356:46 V2 | |||
1166 | testdata/Builtins.lc 356:26-356:32 Type->Type | 1166 | testdata/Builtins.lc 356:26-356:32 Type->Type |
1167 | testdata/Builtins.lc 356:38-356:44 Type->Type | 1167 | testdata/Builtins.lc 356:38-356:44 Type->Type |
1168 | testdata/Builtins.lc 356:1-356:10 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 1168 | testdata/Builtins.lc 356:1-356:10 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b |
1169 | testdata/Builtins.lc 357:18-357:52 Type | 1169 | testdata/Builtins.lc 357:21-357:59 Type |
1170 | testdata/Builtins.lc 357:18-357:52 V1 | 1170 | testdata/Builtins.lc 357:21-357:59 V3 |
1171 | testdata/Builtins.lc 357:23-357:27 Type | 1171 | testdata/Builtins.lc 357:26-357:32 Type->Type |
1172 | testdata/Builtins.lc 357:32-357:38 Type->Type | 1172 | testdata/Builtins.lc 357:21-357:59 V2 |
1173 | testdata/Builtins.lc 357:44-357:50 Type->Type | 1173 | testdata/Builtins.lc 357:39-357:45 Type->Type |
1174 | testdata/Builtins.lc 357:1-357:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a | 1174 | testdata/Builtins.lc 357:51-357:57 Type->Type |
1175 | testdata/Builtins.lc 359:22-359:35 Type | 1175 | testdata/Builtins.lc 357:1-357:16 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b |
1176 | testdata/Builtins.lc 359:6-359:15 'PrimitiveType -> Type->Type | 1176 | testdata/Builtins.lc 358:18-358:52 Type |
1177 | testdata/Builtins.lc 361:28-361:34 Type->Type | 1177 | testdata/Builtins.lc 358:18-358:52 V1 |
1178 | testdata/Builtins.lc 361:36-361:49 Type | 1178 | testdata/Builtins.lc 358:23-358:27 Type |
1179 | testdata/Builtins.lc 361:36-361:45 'PrimitiveType -> Type->Type | 1179 | testdata/Builtins.lc 358:32-358:38 Type->Type |
1180 | testdata/Builtins.lc 361:46-361:47 'PrimitiveType | 1180 | testdata/Builtins.lc 358:44-358:50 Type->Type |
1181 | testdata/Builtins.lc 361:46-361:47 V3 | 1181 | testdata/Builtins.lc 358:1-358:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a |
1182 | testdata/Builtins.lc 361:48-361:49 Type | 1182 | testdata/Builtins.lc 360:22-360:35 Type |
1183 | testdata/Builtins.lc 361:48-361:49 V1 | 1183 | testdata/Builtins.lc 360:6-360:15 'PrimitiveType -> Type->Type |
1184 | testdata/Builtins.lc 361:6-361:21 'PrimitiveType -> Type->Type | 1184 | testdata/Builtins.lc 362:28-362:34 Type->Type |
1185 | testdata/Builtins.lc 363:18-363:59 Type | 1185 | testdata/Builtins.lc 362:36-362:49 Type |
1186 | testdata/Builtins.lc 363:18-363:59 V5 | 1186 | testdata/Builtins.lc 362:36-362:45 'PrimitiveType -> Type->Type |
1187 | testdata/Builtins.lc 363:18-363:59 V4 | 1187 | testdata/Builtins.lc 362:46-362:47 'PrimitiveType |
1188 | testdata/Builtins.lc 363:29-363:38 'PrimitiveType -> Type->Type | 1188 | testdata/Builtins.lc 362:46-362:47 V3 |
1189 | testdata/Builtins.lc 363:18-363:59 'PrimitiveType | 1189 | testdata/Builtins.lc 362:48-362:49 Type |
1190 | testdata/Builtins.lc 363:18-363:59 V2 | 1190 | testdata/Builtins.lc 362:48-362:49 V1 |
1191 | testdata/Builtins.lc 363:46-363:55 'PrimitiveType -> Type->Type | 1191 | testdata/Builtins.lc 362:6-362:21 'PrimitiveType -> Type->Type |
1192 | testdata/Builtins.lc 363:1-363:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b | 1192 | testdata/Builtins.lc 364:18-364:59 Type |
1193 | testdata/Builtins.lc 365:39-365:94 Type | 1193 | testdata/Builtins.lc 364:18-364:59 V5 |
1194 | testdata/Builtins.lc 365:39-365:53 Type->Type | 1194 | testdata/Builtins.lc 364:18-364:59 V4 |
1195 | testdata/Builtins.lc 365:54-365:55 Type | 1195 | testdata/Builtins.lc 364:29-364:38 'PrimitiveType -> Type->Type |
1196 | testdata/Builtins.lc 365:54-365:55 V1 | 1196 | testdata/Builtins.lc 364:18-364:59 'PrimitiveType |
1197 | testdata/Builtins.lc 365:60-365:94 Type | 1197 | testdata/Builtins.lc 364:18-364:59 V2 |
1198 | testdata/Builtins.lc 365:60-365:66 Type | 1198 | testdata/Builtins.lc 364:46-364:55 'PrimitiveType -> Type->Type |
1199 | testdata/Builtins.lc 365:70-365:94 Type | 1199 | testdata/Builtins.lc 364:1-364:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b |
1200 | testdata/Builtins.lc 365:70-365:71 Type | 1200 | testdata/Builtins.lc 366:39-366:94 Type |
1201 | testdata/Builtins.lc 365:75-365:94 Type | 1201 | testdata/Builtins.lc 366:39-366:53 Type->Type |
1202 | testdata/Builtins.lc 365:75-365:90 'PrimitiveType -> Type->Type | 1202 | testdata/Builtins.lc 366:54-366:55 Type |
1203 | testdata/Builtins.lc 365:91-365:92 'PrimitiveType | 1203 | testdata/Builtins.lc 366:54-366:55 V1 |
1204 | testdata/Builtins.lc 365:91-365:92 V5 | 1204 | testdata/Builtins.lc 366:60-366:94 Type |
1205 | testdata/Builtins.lc 365:93-365:94 Type | 1205 | testdata/Builtins.lc 366:60-366:66 Type |
1206 | testdata/Builtins.lc 365:1-365:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) | 1206 | testdata/Builtins.lc 366:70-366:94 Type |
1207 | testdata/Builtins.lc 366:42-366:104 Type | 1207 | testdata/Builtins.lc 366:70-366:71 Type |
1208 | testdata/Builtins.lc 366:42-366:56 Type->Type | 1208 | testdata/Builtins.lc 366:75-366:94 Type |
1209 | testdata/Builtins.lc 366:57-366:58 Type | 1209 | testdata/Builtins.lc 366:75-366:90 'PrimitiveType -> Type->Type |
1210 | testdata/Builtins.lc 366:57-366:58 V3 | 1210 | testdata/Builtins.lc 366:91-366:92 'PrimitiveType |
1211 | testdata/Builtins.lc 366:60-366:104 Type | 1211 | testdata/Builtins.lc 366:91-366:92 V5 |
1212 | testdata/Builtins.lc 366:60-366:61 Type | 1212 | testdata/Builtins.lc 366:93-366:94 Type |
1213 | testdata/Builtins.lc 366:64-366:74 Type | 1213 | testdata/Builtins.lc 366:1-366:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) |
1214 | testdata/Builtins.lc 366:64-366:71 Type->Type | 1214 | testdata/Builtins.lc 367:42-367:104 Type |
1215 | testdata/Builtins.lc 366:72-366:74 Type | 1215 | testdata/Builtins.lc 367:42-367:56 Type->Type |
1216 | testdata/Builtins.lc 366:72-366:74 V2 | 1216 | testdata/Builtins.lc 367:57-367:58 Type |
1217 | testdata/Builtins.lc 366:79-366:104 Type | 1217 | testdata/Builtins.lc 367:57-367:58 V3 |
1218 | testdata/Builtins.lc 366:79-366:81 Type | 1218 | testdata/Builtins.lc 367:60-367:104 Type |
1219 | testdata/Builtins.lc 366:85-366:104 Type | 1219 | testdata/Builtins.lc 367:60-367:61 Type |
1220 | testdata/Builtins.lc 366:85-366:100 'PrimitiveType -> Type->Type | 1220 | testdata/Builtins.lc 367:64-367:74 Type |
1221 | testdata/Builtins.lc 366:101-366:102 'PrimitiveType | 1221 | testdata/Builtins.lc 367:64-367:71 Type->Type |
1222 | testdata/Builtins.lc 366:101-366:102 V6 | 1222 | testdata/Builtins.lc 367:72-367:74 Type |
1223 | testdata/Builtins.lc 366:103-366:104 Type | 1223 | testdata/Builtins.lc 367:72-367:74 V2 |
1224 | testdata/Builtins.lc 366:1-366:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) | 1224 | testdata/Builtins.lc 367:79-367:104 Type |
1225 | testdata/Builtins.lc 368:19-368:77 Type | 1225 | testdata/Builtins.lc 367:79-367:81 Type |
1226 | testdata/Builtins.lc 368:19-368:77 V5 | 1226 | testdata/Builtins.lc 367:85-367:104 Type |
1227 | testdata/Builtins.lc 368:19-368:77 V4 | 1227 | testdata/Builtins.lc 367:85-367:100 'PrimitiveType -> Type->Type |
1228 | testdata/Builtins.lc 368:31-368:37 Type->Type | 1228 | testdata/Builtins.lc 367:101-367:102 'PrimitiveType |
1229 | testdata/Builtins.lc 368:39-368:48 'PrimitiveType -> Type->Type | 1229 | testdata/Builtins.lc 367:101-367:102 V6 |
1230 | testdata/Builtins.lc 368:19-368:77 'PrimitiveType | 1230 | testdata/Builtins.lc 367:103-367:104 Type |
1231 | testdata/Builtins.lc 368:19-368:77 V2 | 1231 | testdata/Builtins.lc 367:1-367:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) |
1232 | testdata/Builtins.lc 368:58-368:73 'PrimitiveType -> Type->Type | 1232 | testdata/Builtins.lc 369:19-369:74 Type |
1233 | testdata/Builtins.lc 369:19-369:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) | 1233 | testdata/Builtins.lc 369:19-369:74 V5 |
1234 | testdata/Builtins.lc 369:19-369:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) | 1234 | testdata/Builtins.lc 369:19-369:74 V4 |
1235 | testdata/Builtins.lc 369:19-369:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) | 1235 | testdata/Builtins.lc 369:31-369:46 'PrimitiveType -> Type->Type |
1236 | testdata/Builtins.lc 369:19-369:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) | 1236 | testdata/Builtins.lc 369:19-369:74 'PrimitiveType |
1237 | testdata/Builtins.lc 369:19-369:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) | 1237 | testdata/Builtins.lc 369:19-369:74 V2 |
1238 | testdata/Builtins.lc 369:19-369:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 1238 | testdata/Builtins.lc 369:55-369:70 'PrimitiveType -> Type->Type |
1239 | testdata/Builtins.lc 369:30-369:42 V1->V1 | 1239 | testdata/Builtins.lc 370:19-370:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) |
1240 | testdata/Builtins.lc 369:30-369:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b | 1240 | testdata/Builtins.lc 370:19-370:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) |
1241 | testdata/Builtins.lc 369:1-369:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) | 1241 | testdata/Builtins.lc 370:19-370:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) |
1242 | testdata/Builtins.lc 371:15-371:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) | 1242 | testdata/Builtins.lc 370:19-370:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) |
1243 | testdata/Builtins.lc 371:1-371:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) | 1243 | testdata/Builtins.lc 370:19-370:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) |
1244 | testdata/Builtins.lc 372:19-372:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) | 1244 | testdata/Builtins.lc 370:19-370:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b |
1245 | testdata/Builtins.lc 372:1-372:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) | 1245 | testdata/Builtins.lc 370:30-370:42 V1->V1 |
1246 | testdata/Builtins.lc 374:6-374:18 Type | 1246 | testdata/Builtins.lc 370:30-370:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b |
1247 | testdata/Builtins.lc 374:21-374:28 'DepthHandler | 1247 | testdata/Builtins.lc 370:1-370:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) |
1248 | testdata/Builtins.lc 374:31-374:43 'DepthHandler | 1248 | testdata/Builtins.lc 372:15-372:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) |
1249 | testdata/Builtins.lc 391:23-401:82 Type->Type | 1249 | testdata/Builtins.lc 372:1-372:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) |
1250 | testdata/Builtins.lc 391:23-401:82 Type | 1250 | testdata/Builtins.lc 373:19-373:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) |
1251 | testdata/Builtins.lc 391:23-391:25 Type | 1251 | testdata/Builtins.lc 373:1-373:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) |
1252 | testdata/Builtins.lc 392:25-401:82 Type | 1252 | testdata/Builtins.lc 375:6-375:18 Type |
1253 | testdata/Builtins.lc 392:25-392:26 Type | 1253 | testdata/Builtins.lc 375:21-375:28 'DepthHandler |
1254 | testdata/Builtins.lc 393:19-401:82 Type | 1254 | testdata/Builtins.lc 375:31-375:43 'DepthHandler |
1255 | testdata/Builtins.lc 393:39-393:45 Type -> Type->Type | 1255 | testdata/Builtins.lc 392:23-402:82 Type->Type |
1256 | testdata/Builtins.lc 393:39-393:45 Type->Type | 1256 | testdata/Builtins.lc 392:23-402:82 Type |
1257 | testdata/Builtins.lc 393:39-393:45 Type | 1257 | testdata/Builtins.lc 392:23-392:25 Type |
1258 | testdata/Builtins.lc 393:19-393:35 Type | 1258 | testdata/Builtins.lc 393:25-402:82 Type |
1259 | testdata/Builtins.lc 394:19-401:82 Type | 1259 | testdata/Builtins.lc 393:25-393:26 Type |
1260 | testdata/Builtins.lc 394:48-399:58 Type -> Type -> Type->Type | 1260 | testdata/Builtins.lc 394:19-402:82 Type |
1261 | testdata/Builtins.lc 394:48-399:58 Type -> Type->Type | 1261 | testdata/Builtins.lc 394:39-394:45 Type -> Type->Type |
1262 | testdata/Builtins.lc 394:48-399:58 Type->Type | 1262 | testdata/Builtins.lc 394:39-394:45 Type->Type |
1263 | testdata/Builtins.lc 394:48-399:58 Type | 1263 | testdata/Builtins.lc 394:39-394:45 Type |
1264 | testdata/Builtins.lc 394:48-394:57 Type->Type | 1264 | testdata/Builtins.lc 394:19-394:35 Type |
1265 | testdata/Builtins.lc 394:48-394:57 Type | 1265 | testdata/Builtins.lc 395:19-402:82 Type |
1266 | testdata/Builtins.lc 394:48-394:57 Type -> Type -> Type->Type | 1266 | testdata/Builtins.lc 395:48-400:58 Type -> Type -> Type->Type |
1267 | testdata/Builtins.lc 399:52-399:58 Type | 1267 | testdata/Builtins.lc 395:48-400:58 Type -> Type->Type |
1268 | testdata/Builtins.lc 399:52-399:58 Type->Type | 1268 | testdata/Builtins.lc 395:48-400:58 Type->Type |
1269 | testdata/Builtins.lc 399:52-399:58 Type -> Type->Type | 1269 | testdata/Builtins.lc 395:48-400:58 Type |
1270 | testdata/Builtins.lc 394:19-394:44 Type | 1270 | testdata/Builtins.lc 395:48-395:57 Type->Type |
1271 | testdata/Builtins.lc 395:19-401:82 Type | 1271 | testdata/Builtins.lc 395:48-395:57 Type |
1272 | testdata/Builtins.lc 395:57-400:70 Type -> Type -> Type -> Type->Type | 1272 | testdata/Builtins.lc 395:48-395:57 Type -> Type -> Type->Type |
1273 | testdata/Builtins.lc 395:57-400:70 Type -> Type -> Type->Type | 1273 | testdata/Builtins.lc 400:52-400:58 Type |
1274 | testdata/Builtins.lc 395:57-400:70 Type -> Type->Type | 1274 | testdata/Builtins.lc 400:52-400:58 Type->Type |
1275 | testdata/Builtins.lc 395:57-400:70 Type->Type | 1275 | testdata/Builtins.lc 400:52-400:58 Type -> Type->Type |
1276 | testdata/Builtins.lc 395:57-400:70 Type | 1276 | testdata/Builtins.lc 395:19-395:44 Type |
1277 | testdata/Builtins.lc 395:57-395:69 Type->Type | 1277 | testdata/Builtins.lc 396:19-402:82 Type |
1278 | testdata/Builtins.lc 395:57-395:69 Type | 1278 | testdata/Builtins.lc 396:57-401:70 Type -> Type -> Type -> Type->Type |
1279 | testdata/Builtins.lc 395:57-395:69 Type -> Type -> Type -> Type->Type | 1279 | testdata/Builtins.lc 396:57-401:70 Type -> Type -> Type->Type |
1280 | testdata/Builtins.lc 400:61-400:70 Type | 1280 | testdata/Builtins.lc 396:57-401:70 Type -> Type->Type |
1281 | testdata/Builtins.lc 400:61-400:70 Type->Type | 1281 | testdata/Builtins.lc 396:57-401:70 Type->Type |
1282 | testdata/Builtins.lc 400:61-400:70 Type -> Type -> Type->Type | 1282 | testdata/Builtins.lc 396:57-401:70 Type |
1283 | testdata/Builtins.lc 395:19-395:53 Type | 1283 | testdata/Builtins.lc 396:57-396:69 Type->Type |
1284 | testdata/Builtins.lc 396:19-401:82 Type | 1284 | testdata/Builtins.lc 396:57-396:69 Type |
1285 | testdata/Builtins.lc 396:66-401:82 Type -> Type -> Type -> Type -> Type->Type | 1285 | testdata/Builtins.lc 396:57-396:69 Type -> Type -> Type -> Type->Type |
1286 | testdata/Builtins.lc 396:66-401:82 Type -> Type -> Type -> Type->Type | 1286 | testdata/Builtins.lc 401:61-401:70 Type |
1287 | testdata/Builtins.lc 396:66-401:82 Type -> Type -> Type->Type | 1287 | testdata/Builtins.lc 401:61-401:70 Type->Type |
1288 | testdata/Builtins.lc 396:66-401:82 Type -> Type->Type | 1288 | testdata/Builtins.lc 401:61-401:70 Type -> Type -> Type->Type |
1289 | testdata/Builtins.lc 396:66-401:82 Type->Type | 1289 | testdata/Builtins.lc 396:19-396:53 Type |
1290 | testdata/Builtins.lc 396:66-401:82 Type | 1290 | testdata/Builtins.lc 397:19-402:82 Type |
1291 | testdata/Builtins.lc 396:66-396:81 Type->Type | 1291 | testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type -> Type -> Type->Type |
1292 | testdata/Builtins.lc 396:66-396:81 Type | 1292 | testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type -> Type->Type |
1293 | testdata/Builtins.lc 396:66-396:81 Type -> Type -> Type -> Type -> Type->Type | 1293 | testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type->Type |
1294 | testdata/Builtins.lc 401:70-401:82 Type | 1294 | testdata/Builtins.lc 397:66-402:82 Type -> Type->Type |
1295 | testdata/Builtins.lc 401:70-401:82 Type->Type | 1295 | testdata/Builtins.lc 397:66-402:82 Type->Type |
1296 | testdata/Builtins.lc 401:70-401:82 Type -> Type -> Type -> Type->Type | 1296 | testdata/Builtins.lc 397:66-402:82 Type |
1297 | testdata/Builtins.lc 396:19-396:62 Type | 1297 | testdata/Builtins.lc 397:66-397:81 Type->Type |
1298 | testdata/Builtins.lc 397:25-397:36 Type | 1298 | testdata/Builtins.lc 397:66-397:81 Type |
1299 | testdata/Builtins.lc 397:34-397:36 Type->Type | 1299 | testdata/Builtins.lc 397:66-397:81 Type -> Type -> Type -> Type -> Type->Type |
1300 | testdata/Builtins.lc 397:34-397:36 Type | 1300 | testdata/Builtins.lc 402:70-402:82 Type |
1301 | testdata/Builtins.lc 397:25-397:30 Type | 1301 | testdata/Builtins.lc 402:70-402:82 Type->Type |
1302 | testdata/Builtins.lc 391:5-391:17 Type->Type | 1302 | testdata/Builtins.lc 402:70-402:82 Type -> Type -> Type -> Type->Type |
1303 | testdata/Builtins.lc 405:18-405:21 Type | 1303 | testdata/Builtins.lc 397:19-397:62 Type |
1304 | testdata/Builtins.lc 405:25-405:53 Type | 1304 | testdata/Builtins.lc 398:25-398:36 Type |
1305 | testdata/Builtins.lc 405:25-405:37 Type | 1305 | testdata/Builtins.lc 398:34-398:36 Type->Type |
1306 | testdata/Builtins.lc 405:41-405:53 Type | 1306 | testdata/Builtins.lc 398:34-398:36 Type |
1307 | testdata/Builtins.lc 405:41-405:45 Type | 1307 | testdata/Builtins.lc 398:25-398:30 Type |
1308 | testdata/Builtins.lc 405:49-405:53 Type | 1308 | testdata/Builtins.lc 392:5-392:17 Type->Type |
1309 | testdata/Builtins.lc 405:6-405:14 'Nat -> 'DepthHandler -> Type->Type | 1309 | testdata/Builtins.lc 406:18-406:21 Type |
1310 | testdata/Builtins.lc 407:20-407:78 Type | 1310 | testdata/Builtins.lc 406:25-406:53 Type |
1311 | testdata/Builtins.lc 407:20-407:78 V3 | 1311 | testdata/Builtins.lc 406:25-406:37 Type |
1312 | testdata/Builtins.lc 407:25-407:30 Type | 1312 | testdata/Builtins.lc 406:41-406:53 Type |
1313 | testdata/Builtins.lc 407:35-407:43 'Nat -> 'DepthHandler -> Type->Type | 1313 | testdata/Builtins.lc 406:41-406:45 Type |
1314 | testdata/Builtins.lc 407:20-407:78 'Nat | 1314 | testdata/Builtins.lc 406:49-406:53 Type |
1315 | testdata/Builtins.lc 407:20-407:78 V2 | 1315 | testdata/Builtins.lc 406:6-406:14 'Nat -> 'DepthHandler -> Type->Type |
1316 | testdata/Builtins.lc 407:53-407:61 'Nat -> 'DepthHandler -> Type->Type | 1316 | testdata/Builtins.lc 408:29-408:35 Type->Type |
1317 | testdata/Builtins.lc 407:64-407:76 'DepthHandler | 1317 | testdata/Builtins.lc 408:37-408:51 Type |
1318 | testdata/Builtins.lc 407:1-407:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b | 1318 | testdata/Builtins.lc 408:37-408:45 'Nat -> 'DepthHandler -> Type->Type |
1319 | testdata/Builtins.lc 409:21-409:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 1319 | testdata/Builtins.lc 408:46-408:47 'Nat |
1320 | testdata/Builtins.lc 409:32-409:46 V1->V1 | 1320 | testdata/Builtins.lc 408:46-408:47 V5 |
1321 | testdata/Builtins.lc 409:32-409:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b | 1321 | testdata/Builtins.lc 408:48-408:49 'DepthHandler |
1322 | testdata/Builtins.lc 409:1-409:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) | 1322 | testdata/Builtins.lc 408:48-408:49 V3 |
1323 | testdata/Builtins.lc 416:21-420:62 Type | 1323 | testdata/Builtins.lc 408:50-408:51 Type |
1324 | testdata/Builtins.lc 416:21-420:62 V7 | 1324 | testdata/Builtins.lc 408:50-408:51 V1 |
1325 | testdata/Builtins.lc 416:25-416:41 Type->Type | 1325 | testdata/Builtins.lc 408:6-408:20 'Nat -> 'DepthHandler -> Type->Type |
1326 | testdata/Builtins.lc 416:21-420:62 V5 | 1326 | testdata/Builtins.lc 410:20-410:78 Type |
1327 | testdata/Builtins.lc 416:21-420:62 V4 | 1327 | testdata/Builtins.lc 410:20-410:78 V3 |
1328 | testdata/Builtins.lc 416:49-416:62 Type -> Type->Type | 1328 | testdata/Builtins.lc 410:25-410:30 Type |
1329 | testdata/Builtins.lc 416:64-416:75 Type | 1329 | testdata/Builtins.lc 410:35-410:43 'Nat -> 'DepthHandler -> Type->Type |
1330 | testdata/Builtins.lc 416:64-416:67 'Nat -> Type->Type | 1330 | testdata/Builtins.lc 410:20-410:78 'Nat |
1331 | testdata/Builtins.lc 416:70-416:75 Type | 1331 | testdata/Builtins.lc 410:20-410:78 V2 |
1332 | testdata/Builtins.lc 417:26-417:31 Type | 1332 | testdata/Builtins.lc 410:53-410:61 'Nat -> 'DepthHandler -> Type->Type |
1333 | testdata/Builtins.lc 419:20-419:33 'PrimitiveType->Type | 1333 | testdata/Builtins.lc 410:64-410:76 'DepthHandler |
1334 | testdata/Builtins.lc 416:21-420:62 'PrimitiveType | 1334 | testdata/Builtins.lc 410:1-410:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b |
1335 | testdata/Builtins.lc 420:20-420:29 'PrimitiveType -> Type->Type | 1335 | testdata/Builtins.lc 412:21-412:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b |
1336 | testdata/Builtins.lc 420:37-420:45 'Nat -> 'DepthHandler -> Type->Type | 1336 | testdata/Builtins.lc 412:32-412:46 V1->V1 |
1337 | testdata/Builtins.lc 420:48-420:60 'DepthHandler | 1337 | testdata/Builtins.lc 412:32-412:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b |
1338 | testdata/Builtins.lc 416:1-416:11 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Fragment (Succ Zero) DefinedDepth a | 1338 | testdata/Builtins.lc 412:1-412:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) |
1339 | testdata/Builtins.lc 422:20-422:56 Type | 1339 | testdata/Builtins.lc 419:21-423:68 Type |
1340 | testdata/Builtins.lc 422:20-422:56 V3 | 1340 | testdata/Builtins.lc 419:21-423:68 V7 |
1341 | testdata/Builtins.lc 422:25-422:29 Type | 1341 | testdata/Builtins.lc 419:25-419:41 Type->Type |
1342 | testdata/Builtins.lc 422:34-422:42 'Nat -> 'DepthHandler -> Type->Type | 1342 | testdata/Builtins.lc 419:21-423:68 V5 |
1343 | testdata/Builtins.lc 422:20-422:56 'Nat | 1343 | testdata/Builtins.lc 419:21-423:68 V4 |
1344 | testdata/Builtins.lc 422:20-422:56 V2 | 1344 | testdata/Builtins.lc 419:49-419:62 Type -> Type->Type |
1345 | testdata/Builtins.lc 422:52-422:56 Type | 1345 | testdata/Builtins.lc 419:64-419:75 Type |
1346 | testdata/Builtins.lc 422:1-422:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool | 1346 | testdata/Builtins.lc 419:64-419:67 'Nat -> Type->Type |
1347 | testdata/Builtins.lc 424:21-424:84 Type | 1347 | testdata/Builtins.lc 419:70-419:75 Type |
1348 | testdata/Builtins.lc 424:21-424:84 V5 | 1348 | testdata/Builtins.lc 420:26-420:31 Type |
1349 | testdata/Builtins.lc 424:26-424:30 Type | 1349 | testdata/Builtins.lc 422:20-422:33 'PrimitiveType->Type |
1350 | testdata/Builtins.lc 424:35-424:41 Type->Type | 1350 | testdata/Builtins.lc 419:21-423:68 'PrimitiveType |
1351 | testdata/Builtins.lc 424:43-424:51 'Nat -> 'DepthHandler -> Type->Type | 1351 | testdata/Builtins.lc 423:20-423:29 'PrimitiveType -> Type->Type |
1352 | testdata/Builtins.lc 424:21-424:84 'Nat | 1352 | testdata/Builtins.lc 423:37-423:51 'Nat -> 'DepthHandler -> Type->Type |
1353 | testdata/Builtins.lc 424:21-424:84 V4 | 1353 | testdata/Builtins.lc 423:54-423:66 'DepthHandler |
1354 | testdata/Builtins.lc 424:21-424:84 'DepthHandler | 1354 | testdata/Builtins.lc 419:1-419:11 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) |
1355 | testdata/Builtins.lc 424:21-424:84 V2 | 1355 | testdata/Builtins.lc 425:20-425:56 Type |
1356 | testdata/Builtins.lc 424:62-424:68 Type->Type | 1356 | testdata/Builtins.lc 425:20-425:56 V3 |
1357 | testdata/Builtins.lc 424:70-424:78 'Nat -> 'DepthHandler -> Type->Type | 1357 | testdata/Builtins.lc 425:25-425:29 Type |
1358 | testdata/Builtins.lc 425:21-425:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) | 1358 | testdata/Builtins.lc 425:34-425:42 'Nat -> 'DepthHandler -> Type->Type |
1359 | testdata/Builtins.lc 425:21-425:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) | 1359 | testdata/Builtins.lc 425:20-425:56 'Nat |
1360 | testdata/Builtins.lc 425:21-425:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) | 1360 | testdata/Builtins.lc 425:20-425:56 V2 |
1361 | testdata/Builtins.lc 425:21-425:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) | 1361 | testdata/Builtins.lc 425:52-425:56 Type |
1362 | testdata/Builtins.lc 425:21-425:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) | 1362 | testdata/Builtins.lc 425:1-425:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool |
1363 | testdata/Builtins.lc 425:21-425:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a | 1363 | testdata/Builtins.lc 427:21-427:82 Type |
1364 | testdata/Builtins.lc 425:35-425:49 V0->'Bool | 1364 | testdata/Builtins.lc 427:21-427:82 V5 |
1365 | testdata/Builtins.lc 425:35-425:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool | 1365 | testdata/Builtins.lc 427:26-427:30 Type |
1366 | testdata/Builtins.lc 425:1-425:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) | 1366 | testdata/Builtins.lc 427:36-427:50 'Nat -> 'DepthHandler -> Type->Type |
1367 | testdata/Builtins.lc 427:17-427:60 Type | 1367 | testdata/Builtins.lc 427:21-427:82 'Nat |
1368 | testdata/Builtins.lc 427:17-427:60 V7 | 1368 | testdata/Builtins.lc 427:21-427:82 V4 |
1369 | testdata/Builtins.lc 427:17-427:60 V6 | 1369 | testdata/Builtins.lc 427:21-427:82 'DepthHandler |
1370 | testdata/Builtins.lc 427:28-427:36 'Nat -> 'DepthHandler -> Type->Type | 1370 | testdata/Builtins.lc 427:21-427:82 V2 |
1371 | testdata/Builtins.lc 427:17-427:60 'Nat | 1371 | testdata/Builtins.lc 427:62-427:76 'Nat -> 'DepthHandler -> Type->Type |
1372 | testdata/Builtins.lc 427:17-427:60 V4 | 1372 | testdata/Builtins.lc 428:21-428:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) |
1373 | testdata/Builtins.lc 427:17-427:60 'DepthHandler | 1373 | testdata/Builtins.lc 428:21-428:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) |
1374 | testdata/Builtins.lc 427:17-427:60 V2 | 1374 | testdata/Builtins.lc 428:21-428:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) |
1375 | testdata/Builtins.lc 427:46-427:54 'Nat -> 'DepthHandler -> Type->Type | 1375 | testdata/Builtins.lc 428:21-428:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) |
1376 | testdata/Builtins.lc 427:1-427:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b | 1376 | testdata/Builtins.lc 428:21-428:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) |
1377 | testdata/Builtins.lc 429:18-429:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 1377 | testdata/Builtins.lc 428:21-428:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a |
1378 | testdata/Builtins.lc 429:29-429:40 V1->V1 | 1378 | testdata/Builtins.lc 428:35-428:49 V0->'Bool |
1379 | testdata/Builtins.lc 429:29-429:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b | 1379 | testdata/Builtins.lc 428:35-428:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool |
1380 | testdata/Builtins.lc 429:1-429:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) | 1380 | testdata/Builtins.lc 428:1-428:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) |
1381 | testdata/Builtins.lc 434:13-434:26 Type->Type | 1381 | testdata/Builtins.lc 430:17-430:60 Type |
1382 | testdata/Builtins.lc 439:13-439:28 Type->Type | 1382 | testdata/Builtins.lc 430:17-430:60 V7 |
1383 | testdata/Builtins.lc 442:10-443:36 Type->Type | 1383 | testdata/Builtins.lc 430:17-430:60 V6 |
1384 | testdata/Builtins.lc 442:10-443:36 Type | 1384 | testdata/Builtins.lc 430:28-430:36 'Nat -> 'DepthHandler -> Type->Type |
1385 | testdata/Builtins.lc 442:10-442:23 Type->Type | 1385 | testdata/Builtins.lc 430:17-430:60 'Nat |
1386 | testdata/Builtins.lc 442:10-442:23 Type | 1386 | testdata/Builtins.lc 430:17-430:60 V4 |
1387 | testdata/Builtins.lc 442:10-442:23 Type -> 'Nat->Type | 1387 | testdata/Builtins.lc 430:17-430:60 'DepthHandler |
1388 | testdata/Builtins.lc 442:10-442:23 'Nat->Type | 1388 | testdata/Builtins.lc 430:17-430:60 V2 |
1389 | testdata/Builtins.lc 442:37-442:44 Type | 1389 | testdata/Builtins.lc 430:46-430:54 'Nat -> 'DepthHandler -> Type->Type |
1390 | testdata/Builtins.lc 443:10-443:36 Type | 1390 | testdata/Builtins.lc 430:1-430:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b |
1391 | testdata/Builtins.lc 443:10-443:23 Type->Type | 1391 | testdata/Builtins.lc 432:18-432:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b |
1392 | testdata/Builtins.lc 443:10-443:23 Type | 1392 | testdata/Builtins.lc 432:29-432:40 V1->V1 |
1393 | testdata/Builtins.lc 443:31-443:36 Type | 1393 | testdata/Builtins.lc 432:29-432:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b |
1394 | testdata/Builtins.lc 441:7-441:20 Type->Type | 1394 | testdata/Builtins.lc 432:1-432:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) |
1395 | testdata/Builtins.lc 441:7-441:65 Type | 1395 | testdata/Builtins.lc 437:13-437:26 Type->Type |
1396 | testdata/Builtins.lc 441:46-441:65 Type | 1396 | testdata/Builtins.lc 442:13-442:28 Type->Type |
1397 | testdata/Builtins.lc 441:46-441:63 Type->Type | 1397 | testdata/Builtins.lc 445:10-446:36 Type->Type |
1398 | testdata/Builtins.lc 441:64-441:65 Type | 1398 | testdata/Builtins.lc 445:10-446:36 Type |
1399 | testdata/Builtins.lc 442:37-443:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a | 1399 | testdata/Builtins.lc 445:10-445:23 Type->Type |
1400 | testdata/Builtins.lc 442:37-443:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 | 1400 | testdata/Builtins.lc 445:10-445:23 Type |
1401 | testdata/Builtins.lc 442:69-442:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) | 1401 | testdata/Builtins.lc 445:10-445:23 Type -> 'Nat->Type |
1402 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) | 1402 | testdata/Builtins.lc 445:10-445:23 'Nat->Type |
1403 | testdata/Builtins.lc 442:69-442:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) | 1403 | testdata/Builtins.lc 445:37-445:44 Type |
1404 | testdata/Builtins.lc 442:69-442:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) | 1404 | testdata/Builtins.lc 446:10-446:36 Type |
1405 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) | 1405 | testdata/Builtins.lc 446:10-446:23 Type->Type |
1406 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) | 1406 | testdata/Builtins.lc 446:10-446:23 Type |
1407 | testdata/Builtins.lc 442:69-442:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) | 1407 | testdata/Builtins.lc 446:31-446:36 Type |
1408 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) | 1408 | testdata/Builtins.lc 444:7-444:20 Type->Type |
1409 | testdata/Builtins.lc 442:69-442:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) | 1409 | testdata/Builtins.lc 444:7-444:65 Type |
1410 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) | 1410 | testdata/Builtins.lc 444:46-444:65 Type |
1411 | testdata/Builtins.lc 442:69-442:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) | 1411 | testdata/Builtins.lc 444:46-444:63 Type->Type |
1412 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) | 1412 | testdata/Builtins.lc 444:64-444:65 Type |
1413 | testdata/Builtins.lc 442:69-442:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a)))))) | 1413 | testdata/Builtins.lc 445:37-446:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a |
1414 | testdata/Builtins.lc 442:69-442:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) | 1414 | testdata/Builtins.lc 445:37-446:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 |
1415 | testdata/Builtins.lc 442:69-442:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) | 1415 | testdata/Builtins.lc 445:69-445:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) |
1416 | testdata/Builtins.lc 442:69-442:76 {a} -> {b:'Nat} -> {c} -> {d} -> {e : a ~ 'VecScalar b 'Bool} -> {f : c ~ 'VecScalar b d} -> {g : 'Num d} -> 'Blending d -> a -> 'FragmentOperation ('Color c) | 1416 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) |
1417 | testdata/Builtins.lc 442:77-442:87 'Blending V1 | 1417 | testdata/Builtins.lc 445:69-445:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) |
1418 | testdata/Builtins.lc 442:77-442:87 {a} -> 'Blending a | 1418 | testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) |
1419 | testdata/Builtins.lc 442:89-442:111 'VecScalar V2 'Bool | 1419 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) |
1420 | testdata/Builtins.lc 442:89-442:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) | 1420 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) |
1421 | testdata/Builtins.lc 442:92-442:96 V0 | 1421 | testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) |
1422 | testdata/Builtins.lc 442:92-442:96 'Bool | 1422 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) |
1423 | testdata/Builtins.lc 442:97-442:101 'Bool | 1423 | testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) |
1424 | testdata/Builtins.lc 442:102-442:106 'Bool | 1424 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) |
1425 | testdata/Builtins.lc 442:107-442:111 'Bool | 1425 | testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) |
1426 | testdata/Builtins.lc 443:31-443:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 | 1426 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) |
1427 | testdata/Builtins.lc 443:60-443:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) | 1427 | testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a)))))) |
1428 | testdata/Builtins.lc 443:60-443:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) | 1428 | testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) |
1429 | testdata/Builtins.lc 443:60-443:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) | 1429 | testdata/Builtins.lc 445:69-445:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) |
1430 | testdata/Builtins.lc 443:60-443:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) | 1430 | testdata/Builtins.lc 445:69-445:76 {a} -> {b:'Nat} -> {c} -> {d} -> {e : a ~ 'VecScalar b 'Bool} -> {f : c ~ 'VecScalar b d} -> {g : 'Num d} -> 'Blending d -> a -> 'FragmentOperation ('Color c) |
1431 | testdata/Builtins.lc 443:68-443:72 'ComparisonFunction | 1431 | testdata/Builtins.lc 445:77-445:87 'Blending V1 |
1432 | testdata/Builtins.lc 443:73-443:77 'Bool | 1432 | testdata/Builtins.lc 445:77-445:87 {a} -> 'Blending a |
1433 | testdata/Builtins.lc 441:29-441:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b | 1433 | testdata/Builtins.lc 445:89-445:111 'VecScalar V2 'Bool |
1434 | testdata/Builtins.lc 450:24-450:27 Type | 1434 | testdata/Builtins.lc 445:89-445:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) |
1435 | testdata/Builtins.lc 450:6-450:17 'Nat -> Type->Type | 1435 | testdata/Builtins.lc 445:92-445:96 V0 |
1436 | testdata/Builtins.lc 451:19-451:109 Type | 1436 | testdata/Builtins.lc 445:92-445:96 'Bool |
1437 | testdata/Builtins.lc 451:19-451:27 Type->Type | 1437 | testdata/Builtins.lc 445:97-445:101 'Bool |
1438 | testdata/Builtins.lc 451:28-451:29 Type | 1438 | testdata/Builtins.lc 445:102-445:106 'Bool |
1439 | testdata/Builtins.lc 451:33-451:39 Type->Type | 1439 | testdata/Builtins.lc 445:107-445:111 'Bool |
1440 | testdata/Builtins.lc 451:41-451:49 'Nat -> 'DepthHandler -> Type->Type | 1440 | testdata/Builtins.lc 446:31-446:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 |
1441 | testdata/Builtins.lc 451:50-451:51 'Nat | 1441 | testdata/Builtins.lc 446:60-446:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) |
1442 | testdata/Builtins.lc 451:19-451:109 'DepthHandler | 1442 | testdata/Builtins.lc 446:60-446:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) |
1443 | testdata/Builtins.lc 451:19-451:109 V2 | 1443 | testdata/Builtins.lc 446:60-446:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) |
1444 | testdata/Builtins.lc 451:55-451:69 Type | 1444 | testdata/Builtins.lc 446:60-446:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) |
1445 | testdata/Builtins.lc 451:55-451:67 Type->Type | 1445 | testdata/Builtins.lc 446:68-446:72 'ComparisonFunction |
1446 | testdata/Builtins.lc 451:68-451:69 Type | 1446 | testdata/Builtins.lc 446:73-446:77 'Bool |
1447 | testdata/Builtins.lc 451:75-451:109 Type | 1447 | testdata/Builtins.lc 444:29-444:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b |
1448 | testdata/Builtins.lc 451:75-451:86 'Nat -> Type->Type | 1448 | testdata/Builtins.lc 453:24-453:27 Type |
1449 | testdata/Builtins.lc 451:87-451:88 'Nat | 1449 | testdata/Builtins.lc 453:6-453:17 'Nat -> Type->Type |
1450 | testdata/Builtins.lc 451:89-451:90 Type | 1450 | testdata/Builtins.lc 454:19-454:108 Type |
1451 | testdata/Builtins.lc 451:94-451:109 Type | 1451 | testdata/Builtins.lc 454:19-454:27 Type->Type |
1452 | testdata/Builtins.lc 451:94-451:105 'Nat -> Type->Type | 1452 | testdata/Builtins.lc 454:28-454:29 Type |
1453 | testdata/Builtins.lc 451:106-451:107 'Nat | 1453 | testdata/Builtins.lc 454:34-454:48 'Nat -> 'DepthHandler -> Type->Type |
1454 | testdata/Builtins.lc 451:108-451:109 Type | 1454 | testdata/Builtins.lc 454:49-454:50 'Nat |
1455 | testdata/Builtins.lc 451:3-451:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b | 1455 | testdata/Builtins.lc 454:19-454:108 'DepthHandler |
1456 | testdata/Builtins.lc 452:20-452:117 Type | 1456 | testdata/Builtins.lc 454:19-454:108 V2 |
1457 | testdata/Builtins.lc 452:20-452:36 Type->Type | 1457 | testdata/Builtins.lc 454:54-454:68 Type |
1458 | testdata/Builtins.lc 452:37-452:38 Type | 1458 | testdata/Builtins.lc 454:54-454:66 Type->Type |
1459 | testdata/Builtins.lc 452:40-452:55 Type->Type | 1459 | testdata/Builtins.lc 454:67-454:68 Type |
1460 | testdata/Builtins.lc 452:20-452:117 V2 | 1460 | testdata/Builtins.lc 454:74-454:108 Type |
1461 | testdata/Builtins.lc 452:59-452:74 Type | 1461 | testdata/Builtins.lc 454:74-454:85 'Nat -> Type->Type |
1462 | testdata/Builtins.lc 452:59-452:70 'Nat -> Type->Type | 1462 | testdata/Builtins.lc 454:86-454:87 'Nat |
1463 | testdata/Builtins.lc 452:71-452:72 'Nat | 1463 | testdata/Builtins.lc 454:88-454:89 Type |
1464 | testdata/Builtins.lc 452:73-452:74 Type | 1464 | testdata/Builtins.lc 454:93-454:108 Type |
1465 | testdata/Builtins.lc 452:77-452:90 Type->Type | 1465 | testdata/Builtins.lc 454:93-454:104 'Nat -> Type->Type |
1466 | testdata/Builtins.lc 452:102-452:117 Type | 1466 | testdata/Builtins.lc 454:105-454:106 'Nat |
1467 | testdata/Builtins.lc 452:102-452:113 'Nat -> Type->Type | 1467 | testdata/Builtins.lc 454:107-454:108 Type |
1468 | testdata/Builtins.lc 452:114-452:115 'Nat | 1468 | testdata/Builtins.lc 454:3-454:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b |
1469 | testdata/Builtins.lc 452:116-452:117 Type | 1469 | testdata/Builtins.lc 455:20-455:117 Type |
1470 | testdata/Builtins.lc 452:3-452:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b | 1470 | testdata/Builtins.lc 455:20-455:36 Type->Type |
1471 | testdata/Builtins.lc 454:34-454:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b | 1471 | testdata/Builtins.lc 455:37-455:38 Type |
1472 | testdata/Builtins.lc 454:50-454:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) | 1472 | testdata/Builtins.lc 455:40-455:55 Type->Type |
1473 | testdata/Builtins.lc 454:50-454:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) | 1473 | testdata/Builtins.lc 455:20-455:117 V2 |
1474 | testdata/Builtins.lc 454:1-454:11 {a:'Nat} -> {b} -> {c:'DepthHandler} -> {d} -> 'FragOps' b -> (d -> 'RemSemantics b) -> 'Stream ('Fragment a c d) -> 'FrameBuffer a b -> 'FrameBuffer a b | 1474 | testdata/Builtins.lc 455:59-455:74 Type |
1475 | testdata/Builtins.lc 456:1-456:20 {a} -> a->a | 1475 | testdata/Builtins.lc 455:59-455:70 'Nat -> Type->Type |
1476 | testdata/Builtins.lc 458:15-458:18 Type | 1476 | testdata/Builtins.lc 455:71-455:72 'Nat |
1477 | testdata/Builtins.lc 458:22-458:34 Type | 1477 | testdata/Builtins.lc 455:73-455:74 Type |
1478 | testdata/Builtins.lc 458:22-458:26 Type | 1478 | testdata/Builtins.lc 455:77-455:90 Type->Type |
1479 | testdata/Builtins.lc 458:30-458:34 Type | 1479 | testdata/Builtins.lc 455:102-455:117 Type |
1480 | testdata/Builtins.lc 458:6-458:11 'Nat -> Type->Type | 1480 | testdata/Builtins.lc 455:102-455:113 'Nat -> Type->Type |
1481 | testdata/Builtins.lc 459:48-460:56 Type | 1481 | testdata/Builtins.lc 455:114-455:115 'Nat |
1482 | testdata/Builtins.lc 459:48-459:51 Type->Type | 1482 | testdata/Builtins.lc 455:116-455:117 Type |
1483 | testdata/Builtins.lc 459:52-459:53 Type | 1483 | testdata/Builtins.lc 455:3-455:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b |
1484 | testdata/Builtins.lc 459:52-459:53 V3 | 1484 | testdata/Builtins.lc 457:34-457:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b |
1485 | testdata/Builtins.lc 459:55-460:56 Type | 1485 | testdata/Builtins.lc 457:50-457:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) |
1486 | testdata/Builtins.lc 459:55-459:60 Type | 1486 | testdata/Builtins.lc 457:50-457:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) |
1487 | testdata/Builtins.lc 459:55-459:60 V2 | 1487 | testdata/Builtins.lc 457:1-457:11 {a:'Nat} -> {b} -> {c:'DepthHandler} -> {d} -> 'FragOps' b -> (d -> 'RemSemantics b) -> 'Stream ('Fragment a c d) -> 'FrameBuffer a b -> 'FrameBuffer a b |
1488 | testdata/Builtins.lc 459:63-459:76 Type | 1488 | testdata/Builtins.lc 459:1-459:20 {a} -> a->a |
1489 | testdata/Builtins.lc 459:63-459:72 'Nat -> Type->Type | 1489 | testdata/Builtins.lc 461:15-461:18 Type |
1490 | testdata/Builtins.lc 459:73-459:74 'Nat | 1490 | testdata/Builtins.lc 461:22-461:34 Type |
1491 | testdata/Builtins.lc 459:73-459:74 V4 | 1491 | testdata/Builtins.lc 461:22-461:26 Type |
1492 | testdata/Builtins.lc 459:75-459:76 Type | 1492 | testdata/Builtins.lc 461:30-461:34 Type |
1493 | testdata/Builtins.lc 460:26-460:56 Type | 1493 | testdata/Builtins.lc 461:6-461:11 'Nat -> Type->Type |
1494 | testdata/Builtins.lc 460:26-460:31 Type | 1494 | testdata/Builtins.lc 462:48-463:56 Type |
1495 | testdata/Builtins.lc 460:36-460:56 Type | 1495 | testdata/Builtins.lc 462:48-462:51 Type->Type |
1496 | testdata/Builtins.lc 460:36-460:41 'Nat -> Type->Type | 1496 | testdata/Builtins.lc 462:52-462:53 Type |
1497 | testdata/Builtins.lc 460:42-460:43 'Nat | 1497 | testdata/Builtins.lc 462:52-462:53 V3 |
1498 | testdata/Builtins.lc 460:42-460:43 V7 | 1498 | testdata/Builtins.lc 462:55-463:56 Type |
1499 | testdata/Builtins.lc 460:45-460:56 Type | 1499 | testdata/Builtins.lc 462:55-462:60 Type |
1500 | testdata/Builtins.lc 460:45-460:50 Type->Type | 1500 | testdata/Builtins.lc 462:55-462:60 V2 |
1501 | testdata/Builtins.lc 460:51-460:56 Type | 1501 | testdata/Builtins.lc 462:63-462:76 Type |
1502 | testdata/Builtins.lc 459:3-459:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) | 1502 | testdata/Builtins.lc 462:63-462:72 'Nat -> Type->Type |
1503 | testdata/Builtins.lc 461:37-461:67 Type | 1503 | testdata/Builtins.lc 462:73-462:74 'Nat |
1504 | testdata/Builtins.lc 461:37-461:42 Type | 1504 | testdata/Builtins.lc 462:73-462:74 V4 |
1505 | testdata/Builtins.lc 461:47-461:67 Type | 1505 | testdata/Builtins.lc 462:75-462:76 Type |
1506 | testdata/Builtins.lc 461:47-461:52 'Nat -> Type->Type | 1506 | testdata/Builtins.lc 463:26-463:56 Type |
1507 | testdata/Builtins.lc 461:53-461:54 'Nat | 1507 | testdata/Builtins.lc 463:26-463:31 Type |
1508 | testdata/Builtins.lc 461:53-461:54 V2 | 1508 | testdata/Builtins.lc 463:36-463:56 Type |
1509 | testdata/Builtins.lc 461:56-461:67 Type | 1509 | testdata/Builtins.lc 463:36-463:41 'Nat -> Type->Type |
1510 | testdata/Builtins.lc 461:56-461:61 Type->Type | 1510 | testdata/Builtins.lc 463:42-463:43 'Nat |
1511 | testdata/Builtins.lc 461:62-461:67 Type | 1511 | testdata/Builtins.lc 463:42-463:43 V7 |
1512 | testdata/Builtins.lc 461:3-461:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) | 1512 | testdata/Builtins.lc 463:45-463:56 Type |
1513 | testdata/Builtins.lc 462:37-462:67 Type | 1513 | testdata/Builtins.lc 463:45-463:50 Type->Type |
1514 | testdata/Builtins.lc 462:37-462:40 Type | 1514 | testdata/Builtins.lc 463:51-463:56 Type |
1515 | testdata/Builtins.lc 462:47-462:67 Type | 1515 | testdata/Builtins.lc 462:3-462:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) |
1516 | testdata/Builtins.lc 462:47-462:52 'Nat -> Type->Type | 1516 | testdata/Builtins.lc 464:37-464:67 Type |
1517 | testdata/Builtins.lc 462:53-462:54 'Nat | 1517 | testdata/Builtins.lc 464:37-464:42 Type |
1518 | testdata/Builtins.lc 462:53-462:54 V2 | 1518 | testdata/Builtins.lc 464:47-464:67 Type |
1519 | testdata/Builtins.lc 462:56-462:67 Type | 1519 | testdata/Builtins.lc 464:47-464:52 'Nat -> Type->Type |
1520 | testdata/Builtins.lc 462:56-462:63 Type->Type | 1520 | testdata/Builtins.lc 464:53-464:54 'Nat |
1521 | testdata/Builtins.lc 462:64-462:67 Type | 1521 | testdata/Builtins.lc 464:53-464:54 V2 |
1522 | testdata/Builtins.lc 462:3-462:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) | 1522 | testdata/Builtins.lc 464:56-464:67 Type |
1523 | testdata/Builtins.lc 465:26-465:54 Type | 1523 | testdata/Builtins.lc 464:56-464:61 Type->Type |
1524 | testdata/Builtins.lc 465:26-465:37 'Nat -> Type->Type | 1524 | testdata/Builtins.lc 464:62-464:67 Type |
1525 | testdata/Builtins.lc 465:26-465:54 V1 | 1525 | testdata/Builtins.lc 464:3-464:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) |
1526 | testdata/Builtins.lc 465:45-465:50 'Nat -> Type->Type | 1526 | testdata/Builtins.lc 465:37-465:67 Type |
1527 | testdata/Builtins.lc 465:3-465:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a | 1527 | testdata/Builtins.lc 465:37-465:40 Type |
1528 | testdata/Builtins.lc 466:26-466:37 'Nat -> Type->Type | 1528 | testdata/Builtins.lc 465:47-465:67 Type |
1529 | testdata/Builtins.lc 466:40-466:74 Type | 1529 | testdata/Builtins.lc 465:47-465:52 'Nat -> Type->Type |
1530 | testdata/Builtins.lc 466:40-466:74 Type -> Type->Type | 1530 | testdata/Builtins.lc 465:53-465:54 'Nat |
1531 | testdata/Builtins.lc 466:41-466:52 Type | 1531 | testdata/Builtins.lc 465:53-465:54 V2 |
1532 | testdata/Builtins.lc 466:41-466:46 Type->Type | 1532 | testdata/Builtins.lc 465:56-465:67 Type |
1533 | testdata/Builtins.lc 466:47-466:52 Type | 1533 | testdata/Builtins.lc 465:56-465:63 Type->Type |
1534 | testdata/Builtins.lc 466:54-466:72 Type | 1534 | testdata/Builtins.lc 465:64-465:67 Type |
1535 | testdata/Builtins.lc 466:54-466:59 Type->Type | 1535 | testdata/Builtins.lc 465:3-465:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) |
1536 | testdata/Builtins.lc 466:61-466:72 Type | 1536 | testdata/Builtins.lc 468:26-468:54 Type |
1537 | testdata/Builtins.lc 466:61-466:64 'Nat -> Type->Type | 1537 | testdata/Builtins.lc 468:26-468:37 'Nat -> Type->Type |
1538 | testdata/Builtins.lc 466:67-466:72 Type | 1538 | testdata/Builtins.lc 468:26-468:54 V1 |
1539 | testdata/Builtins.lc 466:78-466:105 Type | 1539 | testdata/Builtins.lc 468:45-468:50 'Nat -> Type->Type |
1540 | testdata/Builtins.lc 466:78-466:83 'Nat -> Type->Type | 1540 | testdata/Builtins.lc 468:3-468:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a |
1541 | testdata/Builtins.lc 466:87-466:105 Type | ||
1542 | testdata/Builtins.lc 466:87-466:92 Type->Type | ||
1543 | testdata/Builtins.lc 466:94-466:105 Type | ||
1544 | testdata/Builtins.lc 466:94-466:97 'Nat -> Type->Type | ||
1545 | testdata/Builtins.lc 466:100-466:105 Type | ||
1546 | testdata/Builtins.lc 466:3-466:16 'FrameBuffer (Succ Zero) ('Tuple2 ('Depth 'Float) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) | ||
1547 | testdata/Builtins.lc 460:42-466:105 Type | ||
1548 | testdata/Builtins.lc 460:42-460:56 Type | ||
1549 | testdata/Builtins.lc 461:53-466:105 Type | ||
1550 | testdata/Builtins.lc 461:53-461:67 Type | ||
1551 | testdata/Builtins.lc 462:53-466:105 Type | ||
1552 | testdata/Builtins.lc 462:53-462:67 Type | ||
1553 | testdata/Builtins.lc 465:26-466:105 Type | ||
1554 | testdata/Builtins.lc 468:6-468:12 Type | ||
1555 | testdata/Builtins.lc 469:26-469:51 Type | ||
1556 | testdata/Builtins.lc 469:26-469:37 'Nat -> Type->Type | 1541 | testdata/Builtins.lc 469:26-469:37 'Nat -> Type->Type |
1557 | testdata/Builtins.lc 469:26-469:51 'Nat | 1542 | testdata/Builtins.lc 469:40-469:74 Type |
1558 | testdata/Builtins.lc 469:26-469:51 V3 | 1543 | testdata/Builtins.lc 469:40-469:74 Type -> Type->Type |
1559 | testdata/Builtins.lc 469:26-469:51 V1 | 1544 | testdata/Builtins.lc 469:41-469:52 Type |
1560 | testdata/Builtins.lc 469:45-469:51 Type | 1545 | testdata/Builtins.lc 469:41-469:46 Type->Type |
1561 | testdata/Builtins.lc 469:3-469:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output | 1546 | testdata/Builtins.lc 469:47-469:52 Type |
1562 | testdata/Builtins.lc 475:34-475:73 Type | 1547 | testdata/Builtins.lc 469:54-469:72 Type |
1563 | testdata/Builtins.lc 475:34-475:37 Type->Type | 1548 | testdata/Builtins.lc 469:54-469:59 Type->Type |
1564 | testdata/Builtins.lc 475:39-475:55 Type->Type | 1549 | testdata/Builtins.lc 469:61-469:72 Type |
1565 | testdata/Builtins.lc 475:34-475:73 V1 | 1550 | testdata/Builtins.lc 469:61-469:64 'Nat -> Type->Type |
1566 | testdata/Builtins.lc 475:1-475:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a | 1551 | testdata/Builtins.lc 469:67-469:72 Type |
1567 | testdata/Builtins.lc 475:10-475:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a | 1552 | testdata/Builtins.lc 469:78-469:105 Type |
1568 | testdata/Builtins.lc 475:19-475:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a | 1553 | testdata/Builtins.lc 469:78-469:83 'Nat -> Type->Type |
1569 | testdata/Builtins.lc 476:35-476:80 Type | 1554 | testdata/Builtins.lc 469:87-469:105 Type |
1570 | testdata/Builtins.lc 476:35-476:80 V3 | 1555 | testdata/Builtins.lc 469:87-469:92 Type->Type |
1571 | testdata/Builtins.lc 476:39-476:55 Type->Type | 1556 | testdata/Builtins.lc 469:94-469:105 Type |
1572 | testdata/Builtins.lc 476:35-476:80 V1 | 1557 | testdata/Builtins.lc 469:94-469:97 'Nat -> Type->Type |
1573 | testdata/Builtins.lc 476:59-476:62 Type->Type | 1558 | testdata/Builtins.lc 469:100-469:105 Type |
1574 | testdata/Builtins.lc 476:1-476:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b | 1559 | testdata/Builtins.lc 469:3-469:16 'FrameBuffer (Succ Zero) ('Tuple2 ('Depth 'Float) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) |
1575 | testdata/Builtins.lc 476:11-476:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b | 1560 | testdata/Builtins.lc 463:42-469:105 Type |
1576 | testdata/Builtins.lc 476:21-476:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b | 1561 | testdata/Builtins.lc 463:42-463:56 Type |
1577 | testdata/Builtins.lc 477:35-477:75 Type | 1562 | testdata/Builtins.lc 464:53-469:105 Type |
1578 | testdata/Builtins.lc 477:35-477:38 Type->Type | 1563 | testdata/Builtins.lc 464:53-464:67 Type |
1579 | testdata/Builtins.lc 477:35-477:75 V5 | 1564 | testdata/Builtins.lc 465:53-469:105 Type |
1580 | testdata/Builtins.lc 477:35-477:75 V4 | 1565 | testdata/Builtins.lc 465:53-465:67 Type |
1581 | testdata/Builtins.lc 477:46-477:55 'Nat -> Type->Type | 1566 | testdata/Builtins.lc 468:26-469:105 Type |
1582 | testdata/Builtins.lc 477:35-477:75 'Nat | 1567 | testdata/Builtins.lc 471:6-471:12 Type |
1583 | testdata/Builtins.lc 477:35-477:75 V2 | 1568 | testdata/Builtins.lc 472:26-472:51 Type |
1584 | testdata/Builtins.lc 477:1-477:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | 1569 | testdata/Builtins.lc 472:26-472:37 'Nat -> Type->Type |
1585 | testdata/Builtins.lc 477:10-477:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | 1570 | testdata/Builtins.lc 472:26-472:51 'Nat |
1586 | testdata/Builtins.lc 478:35-478:75 Type | 1571 | testdata/Builtins.lc 472:26-472:51 V3 |
1587 | testdata/Builtins.lc 478:35-478:38 Type->Type | 1572 | testdata/Builtins.lc 472:26-472:51 V1 |
1588 | testdata/Builtins.lc 478:35-478:75 V5 | 1573 | testdata/Builtins.lc 472:45-472:51 Type |
1589 | testdata/Builtins.lc 478:35-478:75 V4 | 1574 | testdata/Builtins.lc 472:3-472:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output |
1590 | testdata/Builtins.lc 478:46-478:55 'Nat -> Type->Type | 1575 | testdata/Builtins.lc 478:34-478:73 Type |
1591 | testdata/Builtins.lc 478:35-478:75 'Nat | 1576 | testdata/Builtins.lc 478:34-478:37 Type->Type |
1592 | testdata/Builtins.lc 478:35-478:75 V2 | 1577 | testdata/Builtins.lc 478:39-478:55 Type->Type |
1593 | testdata/Builtins.lc 478:1-478:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | 1578 | testdata/Builtins.lc 478:34-478:73 V1 |
1594 | testdata/Builtins.lc 478:11-478:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | 1579 | testdata/Builtins.lc 478:1-478:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a |
1595 | testdata/Builtins.lc 479:34-479:71 Type | 1580 | testdata/Builtins.lc 478:10-478:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a |
1596 | testdata/Builtins.lc 479:34-479:40 Type->Type | 1581 | testdata/Builtins.lc 478:19-478:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a |
1597 | testdata/Builtins.lc 479:42-479:58 Type->Type | 1582 | testdata/Builtins.lc 479:35-479:80 Type |
1598 | testdata/Builtins.lc 479:34-479:71 V1 | 1583 | testdata/Builtins.lc 479:35-479:80 V3 |
1599 | testdata/Builtins.lc 479:1-479:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a | 1584 | testdata/Builtins.lc 479:39-479:55 Type->Type |
1600 | testdata/Builtins.lc 481:35-481:80 Type | 1585 | testdata/Builtins.lc 479:35-479:80 V1 |
1601 | testdata/Builtins.lc 481:35-481:43 Type->Type | 1586 | testdata/Builtins.lc 479:59-479:62 Type->Type |
1602 | testdata/Builtins.lc 481:35-481:80 V5 | 1587 | testdata/Builtins.lc 479:1-479:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b |
1603 | testdata/Builtins.lc 481:35-481:80 V4 | 1588 | testdata/Builtins.lc 479:11-479:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b |
1604 | testdata/Builtins.lc 481:51-481:60 'Nat -> Type->Type | 1589 | testdata/Builtins.lc 479:21-479:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b |
1605 | testdata/Builtins.lc 481:35-481:80 'Nat | 1590 | testdata/Builtins.lc 480:35-480:75 Type |
1606 | testdata/Builtins.lc 481:35-481:80 V2 | 1591 | testdata/Builtins.lc 480:35-480:38 Type->Type |
1607 | testdata/Builtins.lc 481:1-481:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | 1592 | testdata/Builtins.lc 480:35-480:75 V5 |
1608 | testdata/Builtins.lc 481:11-481:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | 1593 | testdata/Builtins.lc 480:35-480:75 V4 |
1609 | testdata/Builtins.lc 481:20-481:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | 1594 | testdata/Builtins.lc 480:46-480:55 'Nat -> Type->Type |
1610 | testdata/Builtins.lc 482:35-482:80 Type | 1595 | testdata/Builtins.lc 480:35-480:75 'Nat |
1611 | testdata/Builtins.lc 482:35-482:43 Type->Type | 1596 | testdata/Builtins.lc 480:35-480:75 V2 |
1612 | testdata/Builtins.lc 482:35-482:80 V5 | 1597 | testdata/Builtins.lc 480:1-480:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1613 | testdata/Builtins.lc 482:35-482:80 V4 | 1598 | testdata/Builtins.lc 480:10-480:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1614 | testdata/Builtins.lc 482:51-482:60 'Nat -> Type->Type | 1599 | testdata/Builtins.lc 481:35-481:75 Type |
1615 | testdata/Builtins.lc 482:35-482:80 'Nat | 1600 | testdata/Builtins.lc 481:35-481:38 Type->Type |
1616 | testdata/Builtins.lc 482:35-482:80 V2 | 1601 | testdata/Builtins.lc 481:35-481:75 V5 |
1617 | testdata/Builtins.lc 482:1-482:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | 1602 | testdata/Builtins.lc 481:35-481:75 V4 |
1618 | testdata/Builtins.lc 482:12-482:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | 1603 | testdata/Builtins.lc 481:46-481:55 'Nat -> Type->Type |
1619 | testdata/Builtins.lc 482:22-482:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | 1604 | testdata/Builtins.lc 481:35-481:75 'Nat |
1620 | testdata/Builtins.lc 483:35-483:75 Type | 1605 | testdata/Builtins.lc 481:35-481:75 V2 |
1621 | testdata/Builtins.lc 483:35-483:43 Type->Type | 1606 | testdata/Builtins.lc 481:1-481:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1622 | testdata/Builtins.lc 483:35-483:75 V5 | 1607 | testdata/Builtins.lc 481:11-481:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1623 | testdata/Builtins.lc 483:35-483:75 V4 | 1608 | testdata/Builtins.lc 482:34-482:71 Type |
1624 | testdata/Builtins.lc 483:51-483:60 'Nat -> Type->Type | 1609 | testdata/Builtins.lc 482:34-482:40 Type->Type |
1625 | testdata/Builtins.lc 483:35-483:75 'Nat | 1610 | testdata/Builtins.lc 482:42-482:58 Type->Type |
1626 | testdata/Builtins.lc 483:35-483:75 V2 | 1611 | testdata/Builtins.lc 482:34-482:71 V1 |
1627 | testdata/Builtins.lc 483:1-483:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b | 1612 | testdata/Builtins.lc 482:1-482:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a |
1628 | testdata/Builtins.lc 484:35-484:102 Type | 1613 | testdata/Builtins.lc 484:35-484:80 Type |
1629 | testdata/Builtins.lc 484:35-484:43 Type->Type | 1614 | testdata/Builtins.lc 484:35-484:43 Type->Type |
1630 | testdata/Builtins.lc 484:35-484:102 V7 | 1615 | testdata/Builtins.lc 484:35-484:80 V5 |
1631 | testdata/Builtins.lc 484:35-484:102 V6 | 1616 | testdata/Builtins.lc 484:35-484:80 V4 |
1632 | testdata/Builtins.lc 484:51-484:60 'Nat -> Type->Type | 1617 | testdata/Builtins.lc 484:51-484:60 'Nat -> Type->Type |
1633 | testdata/Builtins.lc 484:35-484:102 'Nat | 1618 | testdata/Builtins.lc 484:35-484:80 'Nat |
1634 | testdata/Builtins.lc 484:35-484:102 V4 | 1619 | testdata/Builtins.lc 484:35-484:80 V2 |
1635 | testdata/Builtins.lc 484:35-484:102 V3 | 1620 | testdata/Builtins.lc 484:1-484:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1636 | testdata/Builtins.lc 484:70-484:79 'Nat -> Type->Type | 1621 | testdata/Builtins.lc 484:11-484:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1637 | testdata/Builtins.lc 484:82-484:86 Type | 1622 | testdata/Builtins.lc 484:20-484:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1638 | testdata/Builtins.lc 484:1-484:12 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b | 1623 | testdata/Builtins.lc 485:35-485:80 Type |
1639 | testdata/Builtins.lc 484:14-484:25 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b | ||
1640 | testdata/Builtins.lc 485:35-485:83 Type | ||
1641 | testdata/Builtins.lc 485:35-485:43 Type->Type | 1624 | testdata/Builtins.lc 485:35-485:43 Type->Type |
1642 | testdata/Builtins.lc 485:35-485:83 V5 | 1625 | testdata/Builtins.lc 485:35-485:80 V5 |
1643 | testdata/Builtins.lc 485:35-485:83 V4 | 1626 | testdata/Builtins.lc 485:35-485:80 V4 |
1644 | testdata/Builtins.lc 485:51-485:60 'Nat -> Type->Type | 1627 | testdata/Builtins.lc 485:51-485:60 'Nat -> Type->Type |
1645 | testdata/Builtins.lc 485:35-485:83 'Nat | 1628 | testdata/Builtins.lc 485:35-485:80 'Nat |
1646 | testdata/Builtins.lc 485:35-485:83 V2 | 1629 | testdata/Builtins.lc 485:35-485:80 V2 |
1647 | testdata/Builtins.lc 485:74-485:78 Type | 1630 | testdata/Builtins.lc 485:1-485:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1648 | testdata/Builtins.lc 485:1-485:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b | 1631 | testdata/Builtins.lc 485:12-485:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1649 | testdata/Builtins.lc 485:15-485:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b | 1632 | testdata/Builtins.lc 485:22-485:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1650 | testdata/Builtins.lc 487:34-487:38 Type | 1633 | testdata/Builtins.lc 486:35-486:75 Type |
1651 | testdata/Builtins.lc 487:42-487:54 Type | 1634 | testdata/Builtins.lc 486:35-486:43 Type->Type |
1652 | testdata/Builtins.lc 487:42-487:46 Type | 1635 | testdata/Builtins.lc 486:35-486:75 V5 |
1653 | testdata/Builtins.lc 487:50-487:54 Type | 1636 | testdata/Builtins.lc 486:35-486:75 V4 |
1654 | testdata/Builtins.lc 487:1-487:8 'Bool -> 'Bool->'Bool | 1637 | testdata/Builtins.lc 486:51-486:60 'Nat -> Type->Type |
1655 | testdata/Builtins.lc 487:10-487:16 'Bool -> 'Bool->'Bool | 1638 | testdata/Builtins.lc 486:35-486:75 'Nat |
1656 | testdata/Builtins.lc 487:18-487:25 'Bool -> 'Bool->'Bool | 1639 | testdata/Builtins.lc 486:35-486:75 V2 |
1657 | testdata/Builtins.lc 488:35-488:66 Type | 1640 | testdata/Builtins.lc 486:1-486:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b |
1658 | testdata/Builtins.lc 488:35-488:66 V3 | 1641 | testdata/Builtins.lc 487:35-487:102 Type |
1659 | testdata/Builtins.lc 488:39-488:48 'Nat -> Type->Type | 1642 | testdata/Builtins.lc 487:35-487:43 Type->Type |
1660 | testdata/Builtins.lc 488:35-488:66 'Nat | 1643 | testdata/Builtins.lc 487:35-487:102 V7 |
1661 | testdata/Builtins.lc 488:35-488:66 V1 | 1644 | testdata/Builtins.lc 487:35-487:102 V6 |
1662 | testdata/Builtins.lc 488:51-488:55 Type | 1645 | testdata/Builtins.lc 487:51-487:60 'Nat -> Type->Type |
1663 | testdata/Builtins.lc 488:1-488:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a | 1646 | testdata/Builtins.lc 487:35-487:102 'Nat |
1664 | testdata/Builtins.lc 489:34-489:58 Type | 1647 | testdata/Builtins.lc 487:35-487:102 V4 |
1665 | testdata/Builtins.lc 489:34-489:43 'Nat -> Type->Type | 1648 | testdata/Builtins.lc 487:35-487:102 V3 |
1666 | testdata/Builtins.lc 489:34-489:58 'Nat | 1649 | testdata/Builtins.lc 487:70-487:79 'Nat -> Type->Type |
1667 | testdata/Builtins.lc 489:34-489:58 V1 | 1650 | testdata/Builtins.lc 487:82-487:86 Type |
1668 | testdata/Builtins.lc 489:46-489:50 Type | 1651 | testdata/Builtins.lc 487:1-487:12 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b |
1669 | testdata/Builtins.lc 489:54-489:58 Type | 1652 | testdata/Builtins.lc 487:14-487:25 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b |
1670 | testdata/Builtins.lc 489:1-489:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool | 1653 | testdata/Builtins.lc 488:35-488:83 Type |
1671 | testdata/Builtins.lc 489:10-489:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool | 1654 | testdata/Builtins.lc 488:35-488:43 Type->Type |
1672 | testdata/Builtins.lc 493:35-493:67 Type | 1655 | testdata/Builtins.lc 488:35-488:83 V5 |
1673 | testdata/Builtins.lc 493:35-493:67 V3 | 1656 | testdata/Builtins.lc 488:35-488:83 V4 |
1674 | testdata/Builtins.lc 493:39-493:48 'Nat -> Type->Type | 1657 | testdata/Builtins.lc 488:51-488:60 'Nat -> Type->Type |
1675 | testdata/Builtins.lc 493:35-493:67 'Nat | 1658 | testdata/Builtins.lc 488:35-488:83 'Nat |
1676 | testdata/Builtins.lc 493:35-493:67 V1 | 1659 | testdata/Builtins.lc 488:35-488:83 V2 |
1677 | testdata/Builtins.lc 493:51-493:56 Type | 1660 | testdata/Builtins.lc 488:74-488:78 Type |
1678 | testdata/Builtins.lc 492:1-492:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1661 | testdata/Builtins.lc 488:1-488:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b |
1679 | testdata/Builtins.lc 492:11-492:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1662 | testdata/Builtins.lc 488:15-488:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b |
1680 | testdata/Builtins.lc 492:22-492:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1663 | testdata/Builtins.lc 490:34-490:38 Type |
1681 | testdata/Builtins.lc 492:32-492:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1664 | testdata/Builtins.lc 490:42-490:54 Type |
1682 | testdata/Builtins.lc 492:43-492:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1665 | testdata/Builtins.lc 490:42-490:46 Type |
1683 | testdata/Builtins.lc 492:53-492:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1666 | testdata/Builtins.lc 490:50-490:54 Type |
1684 | testdata/Builtins.lc 492:64-492:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1667 | testdata/Builtins.lc 490:1-490:8 'Bool -> 'Bool->'Bool |
1685 | testdata/Builtins.lc 492:73-492:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1668 | testdata/Builtins.lc 490:10-490:16 'Bool -> 'Bool->'Bool |
1686 | testdata/Builtins.lc 492:83-492:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1669 | testdata/Builtins.lc 490:18-490:25 'Bool -> 'Bool->'Bool |
1687 | testdata/Builtins.lc 492:96-492:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1670 | testdata/Builtins.lc 491:35-491:66 Type |
1688 | testdata/Builtins.lc 492:109-492:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1671 | testdata/Builtins.lc 491:35-491:66 V3 |
1689 | testdata/Builtins.lc 492:118-492:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1672 | testdata/Builtins.lc 491:39-491:48 'Nat -> Type->Type |
1690 | testdata/Builtins.lc 492:128-492:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1673 | testdata/Builtins.lc 491:35-491:66 'Nat |
1691 | testdata/Builtins.lc 492:137-492:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1674 | testdata/Builtins.lc 491:35-491:66 V1 |
1692 | testdata/Builtins.lc 492:147-492:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1675 | testdata/Builtins.lc 491:51-491:55 Type |
1693 | testdata/Builtins.lc 492:156-492:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1676 | testdata/Builtins.lc 491:1-491:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a |
1694 | testdata/Builtins.lc 492:165-492:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1677 | testdata/Builtins.lc 492:34-492:58 Type |
1695 | testdata/Builtins.lc 492:175-492:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1678 | testdata/Builtins.lc 492:34-492:43 'Nat -> Type->Type |
1696 | testdata/Builtins.lc 492:185-492:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1679 | testdata/Builtins.lc 492:34-492:58 'Nat |
1697 | testdata/Builtins.lc 492:195-492:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1680 | testdata/Builtins.lc 492:34-492:58 V1 |
1698 | testdata/Builtins.lc 494:35-494:72 Type | 1681 | testdata/Builtins.lc 492:46-492:50 Type |
1699 | testdata/Builtins.lc 494:35-494:72 V3 | 1682 | testdata/Builtins.lc 492:54-492:58 Type |
1700 | testdata/Builtins.lc 494:39-494:48 'Nat -> Type->Type | 1683 | testdata/Builtins.lc 492:1-492:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool |
1701 | testdata/Builtins.lc 494:35-494:72 'Nat | 1684 | testdata/Builtins.lc 492:10-492:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool |
1702 | testdata/Builtins.lc 494:35-494:72 V1 | 1685 | testdata/Builtins.lc 496:35-496:67 Type |
1703 | testdata/Builtins.lc 494:51-494:56 Type | 1686 | testdata/Builtins.lc 496:35-496:67 V3 |
1704 | testdata/Builtins.lc 494:1-494:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a | 1687 | testdata/Builtins.lc 496:39-496:48 'Nat -> Type->Type |
1705 | testdata/Builtins.lc 494:10-494:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a | 1688 | testdata/Builtins.lc 496:35-496:67 'Nat |
1706 | testdata/Builtins.lc 497:35-497:67 Type | 1689 | testdata/Builtins.lc 496:35-496:67 V1 |
1707 | testdata/Builtins.lc 497:35-497:67 V3 | 1690 | testdata/Builtins.lc 496:51-496:56 Type |
1691 | testdata/Builtins.lc 495:1-495:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1692 | testdata/Builtins.lc 495:11-495:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1693 | testdata/Builtins.lc 495:22-495:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1694 | testdata/Builtins.lc 495:32-495:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1695 | testdata/Builtins.lc 495:43-495:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1696 | testdata/Builtins.lc 495:53-495:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1697 | testdata/Builtins.lc 495:64-495:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1698 | testdata/Builtins.lc 495:73-495:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1699 | testdata/Builtins.lc 495:83-495:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1700 | testdata/Builtins.lc 495:96-495:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1701 | testdata/Builtins.lc 495:109-495:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1702 | testdata/Builtins.lc 495:118-495:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1703 | testdata/Builtins.lc 495:128-495:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1704 | testdata/Builtins.lc 495:137-495:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1705 | testdata/Builtins.lc 495:147-495:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1706 | testdata/Builtins.lc 495:156-495:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1707 | testdata/Builtins.lc 495:165-495:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1708 | testdata/Builtins.lc 495:175-495:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1709 | testdata/Builtins.lc 495:185-495:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1710 | testdata/Builtins.lc 495:195-495:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1711 | testdata/Builtins.lc 497:35-497:72 Type | ||
1712 | testdata/Builtins.lc 497:35-497:72 V3 | ||
1708 | testdata/Builtins.lc 497:39-497:48 'Nat -> Type->Type | 1713 | testdata/Builtins.lc 497:39-497:48 'Nat -> Type->Type |
1709 | testdata/Builtins.lc 497:35-497:67 'Nat | 1714 | testdata/Builtins.lc 497:35-497:72 'Nat |
1710 | testdata/Builtins.lc 497:35-497:67 V1 | 1715 | testdata/Builtins.lc 497:35-497:72 V1 |
1711 | testdata/Builtins.lc 497:51-497:56 Type | 1716 | testdata/Builtins.lc 497:51-497:56 Type |
1712 | testdata/Builtins.lc 496:1-496:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1717 | testdata/Builtins.lc 497:1-497:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a |
1713 | testdata/Builtins.lc 496:12-496:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1718 | testdata/Builtins.lc 497:10-497:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a |
1714 | testdata/Builtins.lc 496:23-496:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1719 | testdata/Builtins.lc 500:35-500:67 Type |
1715 | testdata/Builtins.lc 496:34-496:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1720 | testdata/Builtins.lc 500:35-500:67 V3 |
1716 | testdata/Builtins.lc 496:49-496:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1717 | testdata/Builtins.lc 496:59-496:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
1718 | testdata/Builtins.lc 498:35-498:75 Type | ||
1719 | testdata/Builtins.lc 498:35-498:38 Type->Type | ||
1720 | testdata/Builtins.lc 498:35-498:75 V5 | ||
1721 | testdata/Builtins.lc 498:35-498:75 V4 | ||
1722 | testdata/Builtins.lc 498:46-498:55 'Nat -> Type->Type | ||
1723 | testdata/Builtins.lc 498:35-498:75 'Nat | ||
1724 | testdata/Builtins.lc 498:35-498:75 V2 | ||
1725 | testdata/Builtins.lc 498:1-498:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | ||
1726 | testdata/Builtins.lc 498:10-498:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b | ||
1727 | testdata/Builtins.lc 499:35-499:75 Type | ||
1728 | testdata/Builtins.lc 499:35-499:38 Type->Type | ||
1729 | testdata/Builtins.lc 499:35-499:75 V5 | ||
1730 | testdata/Builtins.lc 499:35-499:75 V4 | ||
1731 | testdata/Builtins.lc 499:46-499:55 'Nat -> Type->Type | ||
1732 | testdata/Builtins.lc 499:35-499:75 'Nat | ||
1733 | testdata/Builtins.lc 499:35-499:75 V2 | ||
1734 | testdata/Builtins.lc 499:1-499:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | ||
1735 | testdata/Builtins.lc 499:11-499:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b | ||
1736 | testdata/Builtins.lc 500:35-500:89 Type | ||
1737 | testdata/Builtins.lc 500:35-500:89 V5 | ||
1738 | testdata/Builtins.lc 500:39-500:48 'Nat -> Type->Type | 1721 | testdata/Builtins.lc 500:39-500:48 'Nat -> Type->Type |
1739 | testdata/Builtins.lc 500:35-500:89 'Nat | 1722 | testdata/Builtins.lc 500:35-500:67 'Nat |
1740 | testdata/Builtins.lc 500:35-500:89 V3 | 1723 | testdata/Builtins.lc 500:35-500:67 V1 |
1741 | testdata/Builtins.lc 500:51-500:56 Type | 1724 | testdata/Builtins.lc 500:51-500:56 Type |
1742 | testdata/Builtins.lc 500:35-500:89 V2 | 1725 | testdata/Builtins.lc 499:1-499:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1743 | testdata/Builtins.lc 500:62-500:71 'Nat -> Type->Type | 1726 | testdata/Builtins.lc 499:12-499:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1744 | testdata/Builtins.lc 500:74-500:78 Type | 1727 | testdata/Builtins.lc 499:23-499:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1745 | testdata/Builtins.lc 500:1-500:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c | 1728 | testdata/Builtins.lc 499:34-499:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1746 | testdata/Builtins.lc 500:12-500:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c | 1729 | testdata/Builtins.lc 499:49-499:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1747 | testdata/Builtins.lc 501:35-501:73 Type | 1730 | testdata/Builtins.lc 499:59-499:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1748 | testdata/Builtins.lc 501:35-501:41 Type->Type | 1731 | testdata/Builtins.lc 501:35-501:75 Type |
1749 | testdata/Builtins.lc 501:35-501:73 V5 | 1732 | testdata/Builtins.lc 501:35-501:38 Type->Type |
1750 | testdata/Builtins.lc 501:35-501:73 V4 | 1733 | testdata/Builtins.lc 501:35-501:75 V5 |
1751 | testdata/Builtins.lc 501:49-501:58 'Nat -> Type->Type | 1734 | testdata/Builtins.lc 501:35-501:75 V4 |
1752 | testdata/Builtins.lc 501:35-501:73 'Nat | 1735 | testdata/Builtins.lc 501:46-501:55 'Nat -> Type->Type |
1753 | testdata/Builtins.lc 501:35-501:73 V2 | 1736 | testdata/Builtins.lc 501:35-501:75 'Nat |
1754 | testdata/Builtins.lc 501:1-501:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b | 1737 | testdata/Builtins.lc 501:35-501:75 V2 |
1755 | testdata/Builtins.lc 501:10-501:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b | 1738 | testdata/Builtins.lc 501:1-501:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1756 | testdata/Builtins.lc 502:35-502:72 Type | 1739 | testdata/Builtins.lc 501:10-501:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b |
1757 | testdata/Builtins.lc 502:35-502:72 V3 | 1740 | testdata/Builtins.lc 502:35-502:75 Type |
1758 | testdata/Builtins.lc 502:39-502:48 'Nat -> Type->Type | 1741 | testdata/Builtins.lc 502:35-502:38 Type->Type |
1759 | testdata/Builtins.lc 502:35-502:72 'Nat | 1742 | testdata/Builtins.lc 502:35-502:75 V5 |
1760 | testdata/Builtins.lc 502:35-502:72 V1 | 1743 | testdata/Builtins.lc 502:35-502:75 V4 |
1761 | testdata/Builtins.lc 502:51-502:56 Type | 1744 | testdata/Builtins.lc 502:46-502:55 'Nat -> Type->Type |
1762 | testdata/Builtins.lc 502:66-502:72 Type -> Type->Type | 1745 | testdata/Builtins.lc 502:35-502:75 'Nat |
1763 | testdata/Builtins.lc 502:1-502:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a | 1746 | testdata/Builtins.lc 502:35-502:75 V2 |
1764 | testdata/Builtins.lc 503:35-503:80 Type | 1747 | testdata/Builtins.lc 502:1-502:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1765 | testdata/Builtins.lc 503:35-503:38 Type->Type | 1748 | testdata/Builtins.lc 502:11-502:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b |
1766 | testdata/Builtins.lc 503:35-503:80 V5 | 1749 | testdata/Builtins.lc 503:35-503:89 Type |
1767 | testdata/Builtins.lc 503:35-503:80 V4 | 1750 | testdata/Builtins.lc 503:35-503:89 V5 |
1768 | testdata/Builtins.lc 503:46-503:55 'Nat -> Type->Type | 1751 | testdata/Builtins.lc 503:39-503:48 'Nat -> Type->Type |
1769 | testdata/Builtins.lc 503:35-503:80 'Nat | 1752 | testdata/Builtins.lc 503:35-503:89 'Nat |
1770 | testdata/Builtins.lc 503:35-503:80 V2 | 1753 | testdata/Builtins.lc 503:35-503:89 V3 |
1771 | testdata/Builtins.lc 503:1-503:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b | 1754 | testdata/Builtins.lc 503:51-503:56 Type |
1772 | testdata/Builtins.lc 504:35-504:80 Type | 1755 | testdata/Builtins.lc 503:35-503:89 V2 |
1773 | testdata/Builtins.lc 504:35-504:38 Type->Type | 1756 | testdata/Builtins.lc 503:62-503:71 'Nat -> Type->Type |
1774 | testdata/Builtins.lc 504:35-504:80 V5 | 1757 | testdata/Builtins.lc 503:74-503:78 Type |
1775 | testdata/Builtins.lc 504:35-504:80 V4 | 1758 | testdata/Builtins.lc 503:1-503:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c |
1776 | testdata/Builtins.lc 504:46-504:55 'Nat -> Type->Type | 1759 | testdata/Builtins.lc 503:12-503:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c |
1777 | testdata/Builtins.lc 504:35-504:80 'Nat | 1760 | testdata/Builtins.lc 504:35-504:73 Type |
1778 | testdata/Builtins.lc 504:35-504:80 V2 | 1761 | testdata/Builtins.lc 504:35-504:41 Type->Type |
1779 | testdata/Builtins.lc 504:1-504:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b | 1762 | testdata/Builtins.lc 504:35-504:73 V5 |
1780 | testdata/Builtins.lc 505:35-505:77 Type | 1763 | testdata/Builtins.lc 504:35-504:73 V4 |
1781 | testdata/Builtins.lc 505:35-505:77 V3 | 1764 | testdata/Builtins.lc 504:49-504:58 'Nat -> Type->Type |
1765 | testdata/Builtins.lc 504:35-504:73 'Nat | ||
1766 | testdata/Builtins.lc 504:35-504:73 V2 | ||
1767 | testdata/Builtins.lc 504:1-504:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b | ||
1768 | testdata/Builtins.lc 504:10-504:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b | ||
1769 | testdata/Builtins.lc 505:35-505:72 Type | ||
1770 | testdata/Builtins.lc 505:35-505:72 V3 | ||
1782 | testdata/Builtins.lc 505:39-505:48 'Nat -> Type->Type | 1771 | testdata/Builtins.lc 505:39-505:48 'Nat -> Type->Type |
1783 | testdata/Builtins.lc 505:35-505:77 'Nat | 1772 | testdata/Builtins.lc 505:35-505:72 'Nat |
1784 | testdata/Builtins.lc 505:35-505:77 V1 | 1773 | testdata/Builtins.lc 505:35-505:72 V1 |
1785 | testdata/Builtins.lc 505:51-505:56 Type | 1774 | testdata/Builtins.lc 505:51-505:56 Type |
1786 | testdata/Builtins.lc 505:1-505:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a | 1775 | testdata/Builtins.lc 505:66-505:72 Type -> Type->Type |
1787 | testdata/Builtins.lc 506:35-506:81 Type | 1776 | testdata/Builtins.lc 505:1-505:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a |
1788 | testdata/Builtins.lc 506:35-506:81 V3 | 1777 | testdata/Builtins.lc 506:35-506:80 Type |
1789 | testdata/Builtins.lc 506:39-506:48 'Nat -> Type->Type | 1778 | testdata/Builtins.lc 506:35-506:38 Type->Type |
1790 | testdata/Builtins.lc 506:35-506:81 'Nat | 1779 | testdata/Builtins.lc 506:35-506:80 V5 |
1791 | testdata/Builtins.lc 506:35-506:81 V1 | 1780 | testdata/Builtins.lc 506:35-506:80 V4 |
1792 | testdata/Builtins.lc 506:51-506:56 Type | 1781 | testdata/Builtins.lc 506:46-506:55 'Nat -> Type->Type |
1793 | testdata/Builtins.lc 506:71-506:76 Type | 1782 | testdata/Builtins.lc 506:35-506:80 'Nat |
1794 | testdata/Builtins.lc 506:1-506:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a | 1783 | testdata/Builtins.lc 506:35-506:80 V2 |
1795 | testdata/Builtins.lc 507:35-507:99 Type | 1784 | testdata/Builtins.lc 506:1-506:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b |
1796 | testdata/Builtins.lc 507:35-507:99 V5 | 1785 | testdata/Builtins.lc 507:35-507:80 Type |
1797 | testdata/Builtins.lc 507:39-507:48 'Nat -> Type->Type | 1786 | testdata/Builtins.lc 507:35-507:38 Type->Type |
1798 | testdata/Builtins.lc 507:35-507:99 'Nat | 1787 | testdata/Builtins.lc 507:35-507:80 V5 |
1799 | testdata/Builtins.lc 507:35-507:99 V3 | 1788 | testdata/Builtins.lc 507:35-507:80 V4 |
1800 | testdata/Builtins.lc 507:51-507:56 Type | 1789 | testdata/Builtins.lc 507:46-507:55 'Nat -> Type->Type |
1801 | testdata/Builtins.lc 507:35-507:99 V2 | 1790 | testdata/Builtins.lc 507:35-507:80 'Nat |
1802 | testdata/Builtins.lc 507:62-507:71 'Nat -> Type->Type | 1791 | testdata/Builtins.lc 507:35-507:80 V2 |
1803 | testdata/Builtins.lc 507:74-507:78 Type | 1792 | testdata/Builtins.lc 507:1-507:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b |
1804 | testdata/Builtins.lc 507:1-507:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a | 1793 | testdata/Builtins.lc 508:35-508:77 Type |
1805 | testdata/Builtins.lc 508:35-508:68 Type | 1794 | testdata/Builtins.lc 508:35-508:77 V3 |
1806 | testdata/Builtins.lc 508:35-508:68 V3 | 1795 | testdata/Builtins.lc 508:39-508:48 'Nat -> Type->Type |
1807 | testdata/Builtins.lc 508:39-508:44 'Nat -> Type->Type | 1796 | testdata/Builtins.lc 508:35-508:77 'Nat |
1808 | testdata/Builtins.lc 508:35-508:68 'Nat | 1797 | testdata/Builtins.lc 508:35-508:77 V1 |
1809 | testdata/Builtins.lc 508:35-508:68 V1 | 1798 | testdata/Builtins.lc 508:51-508:56 Type |
1810 | testdata/Builtins.lc 508:47-508:52 Type | 1799 | testdata/Builtins.lc 508:1-508:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a |
1811 | testdata/Builtins.lc 508:1-508:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a | 1800 | testdata/Builtins.lc 509:35-509:81 Type |
1812 | testdata/Builtins.lc 509:35-509:76 Type | 1801 | testdata/Builtins.lc 509:35-509:81 V3 |
1813 | testdata/Builtins.lc 509:35-509:76 V3 | ||
1814 | testdata/Builtins.lc 509:39-509:48 'Nat -> Type->Type | 1802 | testdata/Builtins.lc 509:39-509:48 'Nat -> Type->Type |
1815 | testdata/Builtins.lc 509:35-509:76 'Nat | 1803 | testdata/Builtins.lc 509:35-509:81 'Nat |
1816 | testdata/Builtins.lc 509:35-509:76 V1 | 1804 | testdata/Builtins.lc 509:35-509:81 V1 |
1817 | testdata/Builtins.lc 509:51-509:56 Type | 1805 | testdata/Builtins.lc 509:51-509:56 Type |
1818 | testdata/Builtins.lc 509:61-509:66 Type | 1806 | testdata/Builtins.lc 509:71-509:76 Type |
1819 | testdata/Builtins.lc 509:1-509:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a | 1807 | testdata/Builtins.lc 509:1-509:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a |
1820 | testdata/Builtins.lc 510:35-510:73 Type | 1808 | testdata/Builtins.lc 510:35-510:99 Type |
1821 | testdata/Builtins.lc 510:35-510:73 V3 | 1809 | testdata/Builtins.lc 510:35-510:99 V5 |
1822 | testdata/Builtins.lc 510:39-510:44 'Nat -> Type->Type | 1810 | testdata/Builtins.lc 510:39-510:48 'Nat -> Type->Type |
1823 | testdata/Builtins.lc 510:35-510:73 'Nat | 1811 | testdata/Builtins.lc 510:35-510:99 'Nat |
1824 | testdata/Builtins.lc 510:35-510:73 V1 | 1812 | testdata/Builtins.lc 510:35-510:99 V3 |
1825 | testdata/Builtins.lc 510:47-510:52 Type | 1813 | testdata/Builtins.lc 510:51-510:56 Type |
1826 | testdata/Builtins.lc 510:1-510:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a | 1814 | testdata/Builtins.lc 510:35-510:99 V2 |
1827 | testdata/Builtins.lc 511:35-511:85 Type | 1815 | testdata/Builtins.lc 510:62-510:71 'Nat -> Type->Type |
1828 | testdata/Builtins.lc 511:35-511:85 V3 | 1816 | testdata/Builtins.lc 510:74-510:78 Type |
1829 | testdata/Builtins.lc 511:39-511:48 'Nat -> Type->Type | 1817 | testdata/Builtins.lc 510:1-510:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a |
1830 | testdata/Builtins.lc 511:35-511:85 'Nat | 1818 | testdata/Builtins.lc 511:35-511:68 Type |
1831 | testdata/Builtins.lc 511:35-511:85 V1 | 1819 | testdata/Builtins.lc 511:35-511:68 V3 |
1832 | testdata/Builtins.lc 511:51-511:56 Type | 1820 | testdata/Builtins.lc 511:39-511:44 'Nat -> Type->Type |
1833 | testdata/Builtins.lc 511:61-511:66 Type | 1821 | testdata/Builtins.lc 511:35-511:68 'Nat |
1834 | testdata/Builtins.lc 511:70-511:75 Type | 1822 | testdata/Builtins.lc 511:35-511:68 V1 |
1835 | testdata/Builtins.lc 511:1-511:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a | 1823 | testdata/Builtins.lc 511:47-511:52 Type |
1836 | testdata/Builtins.lc 514:34-514:70 Type | 1824 | testdata/Builtins.lc 511:1-511:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a |
1837 | testdata/Builtins.lc 514:34-514:43 'Nat -> Type->Type | 1825 | testdata/Builtins.lc 512:35-512:76 Type |
1838 | testdata/Builtins.lc 514:34-514:70 'Nat | 1826 | testdata/Builtins.lc 512:35-512:76 V3 |
1839 | testdata/Builtins.lc 514:34-514:70 V1 | 1827 | testdata/Builtins.lc 512:39-512:48 'Nat -> Type->Type |
1840 | testdata/Builtins.lc 514:46-514:51 Type | 1828 | testdata/Builtins.lc 512:35-512:76 'Nat |
1841 | testdata/Builtins.lc 514:55-514:64 'Nat -> Type->Type | 1829 | testdata/Builtins.lc 512:35-512:76 V1 |
1842 | testdata/Builtins.lc 514:67-514:70 Type | 1830 | testdata/Builtins.lc 512:51-512:56 Type |
1843 | testdata/Builtins.lc 514:1-514:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int | 1831 | testdata/Builtins.lc 512:61-512:66 Type |
1844 | testdata/Builtins.lc 515:34-515:71 Type | 1832 | testdata/Builtins.lc 512:1-512:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a |
1845 | testdata/Builtins.lc 515:34-515:43 'Nat -> Type->Type | 1833 | testdata/Builtins.lc 513:35-513:73 Type |
1846 | testdata/Builtins.lc 515:34-515:71 'Nat | 1834 | testdata/Builtins.lc 513:35-513:73 V3 |
1847 | testdata/Builtins.lc 515:34-515:71 V1 | 1835 | testdata/Builtins.lc 513:39-513:44 'Nat -> Type->Type |
1848 | testdata/Builtins.lc 515:46-515:51 Type | 1836 | testdata/Builtins.lc 513:35-513:73 'Nat |
1849 | testdata/Builtins.lc 515:55-515:64 'Nat -> Type->Type | 1837 | testdata/Builtins.lc 513:35-513:73 V1 |
1850 | testdata/Builtins.lc 515:67-515:71 Type | 1838 | testdata/Builtins.lc 513:47-513:52 Type |
1851 | testdata/Builtins.lc 515:1-515:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word | 1839 | testdata/Builtins.lc 513:1-513:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a |
1852 | testdata/Builtins.lc 516:34-516:72 Type | 1840 | testdata/Builtins.lc 514:35-514:85 Type |
1853 | testdata/Builtins.lc 516:34-516:43 'Nat -> Type->Type | 1841 | testdata/Builtins.lc 514:35-514:85 V3 |
1854 | testdata/Builtins.lc 516:34-516:72 'Nat | 1842 | testdata/Builtins.lc 514:39-514:48 'Nat -> Type->Type |
1855 | testdata/Builtins.lc 516:34-516:72 V1 | 1843 | testdata/Builtins.lc 514:35-514:85 'Nat |
1856 | testdata/Builtins.lc 516:46-516:49 Type | 1844 | testdata/Builtins.lc 514:35-514:85 V1 |
1857 | testdata/Builtins.lc 516:55-516:64 'Nat -> Type->Type | 1845 | testdata/Builtins.lc 514:51-514:56 Type |
1858 | testdata/Builtins.lc 516:67-516:72 Type | 1846 | testdata/Builtins.lc 514:61-514:66 Type |
1859 | testdata/Builtins.lc 516:1-516:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float | 1847 | testdata/Builtins.lc 514:70-514:75 Type |
1860 | testdata/Builtins.lc 517:34-517:72 Type | 1848 | testdata/Builtins.lc 514:1-514:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a |
1849 | testdata/Builtins.lc 517:34-517:70 Type | ||
1861 | testdata/Builtins.lc 517:34-517:43 'Nat -> Type->Type | 1850 | testdata/Builtins.lc 517:34-517:43 'Nat -> Type->Type |
1862 | testdata/Builtins.lc 517:34-517:72 'Nat | 1851 | testdata/Builtins.lc 517:34-517:70 'Nat |
1863 | testdata/Builtins.lc 517:34-517:72 V1 | 1852 | testdata/Builtins.lc 517:34-517:70 V1 |
1864 | testdata/Builtins.lc 517:46-517:50 Type | 1853 | testdata/Builtins.lc 517:46-517:51 Type |
1865 | testdata/Builtins.lc 517:55-517:64 'Nat -> Type->Type | 1854 | testdata/Builtins.lc 517:55-517:64 'Nat -> Type->Type |
1866 | testdata/Builtins.lc 517:67-517:72 Type | 1855 | testdata/Builtins.lc 517:67-517:70 Type |
1867 | testdata/Builtins.lc 517:1-517:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float | 1856 | testdata/Builtins.lc 517:1-517:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int |
1868 | testdata/Builtins.lc 519:35-519:71 Type | 1857 | testdata/Builtins.lc 518:34-518:71 Type |
1869 | testdata/Builtins.lc 519:35-519:71 V3 | 1858 | testdata/Builtins.lc 518:34-518:43 'Nat -> Type->Type |
1870 | testdata/Builtins.lc 519:39-519:48 'Nat -> Type->Type | 1859 | testdata/Builtins.lc 518:34-518:71 'Nat |
1871 | testdata/Builtins.lc 519:35-519:71 'Nat | 1860 | testdata/Builtins.lc 518:34-518:71 V1 |
1872 | testdata/Builtins.lc 519:35-519:71 V1 | 1861 | testdata/Builtins.lc 518:46-518:51 Type |
1873 | testdata/Builtins.lc 519:51-519:56 Type | 1862 | testdata/Builtins.lc 518:55-518:64 'Nat -> Type->Type |
1874 | testdata/Builtins.lc 519:66-519:71 Type | 1863 | testdata/Builtins.lc 518:67-518:71 Type |
1875 | testdata/Builtins.lc 519:1-519:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float | 1864 | testdata/Builtins.lc 518:1-518:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word |
1876 | testdata/Builtins.lc 520:35-520:76 Type | 1865 | testdata/Builtins.lc 519:34-519:72 Type |
1877 | testdata/Builtins.lc 520:35-520:76 V3 | 1866 | testdata/Builtins.lc 519:34-519:43 'Nat -> Type->Type |
1878 | testdata/Builtins.lc 520:39-520:48 'Nat -> Type->Type | 1867 | testdata/Builtins.lc 519:34-519:72 'Nat |
1879 | testdata/Builtins.lc 520:35-520:76 'Nat | 1868 | testdata/Builtins.lc 519:34-519:72 V1 |
1880 | testdata/Builtins.lc 520:35-520:76 V1 | 1869 | testdata/Builtins.lc 519:46-519:49 Type |
1881 | testdata/Builtins.lc 520:51-520:56 Type | 1870 | testdata/Builtins.lc 519:55-519:64 'Nat -> Type->Type |
1882 | testdata/Builtins.lc 520:71-520:76 Type | 1871 | testdata/Builtins.lc 519:67-519:72 Type |
1883 | testdata/Builtins.lc 520:1-520:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float | 1872 | testdata/Builtins.lc 519:1-519:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float |
1884 | testdata/Builtins.lc 520:15-520:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float | 1873 | testdata/Builtins.lc 520:34-520:72 Type |
1885 | testdata/Builtins.lc 521:35-521:72 Type | 1874 | testdata/Builtins.lc 520:34-520:43 'Nat -> Type->Type |
1886 | testdata/Builtins.lc 521:35-521:72 V1 | 1875 | testdata/Builtins.lc 520:34-520:72 'Nat |
1887 | testdata/Builtins.lc 521:39-521:56 Type | 1876 | testdata/Builtins.lc 520:34-520:72 V1 |
1888 | testdata/Builtins.lc 521:39-521:48 'Nat -> Type->Type | 1877 | testdata/Builtins.lc 520:46-520:50 Type |
1889 | testdata/Builtins.lc 521:51-521:56 Type | 1878 | testdata/Builtins.lc 520:55-520:64 'Nat -> Type->Type |
1890 | testdata/Builtins.lc 521:1-521:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a | 1879 | testdata/Builtins.lc 520:67-520:72 Type |
1891 | testdata/Builtins.lc 522:35-522:67 Type | 1880 | testdata/Builtins.lc 520:1-520:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float |
1892 | testdata/Builtins.lc 522:35-522:67 V3 | 1881 | testdata/Builtins.lc 522:35-522:71 Type |
1882 | testdata/Builtins.lc 522:35-522:71 V3 | ||
1893 | testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type | 1883 | testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type |
1894 | testdata/Builtins.lc 522:35-522:67 'Nat | 1884 | testdata/Builtins.lc 522:35-522:71 'Nat |
1895 | testdata/Builtins.lc 522:35-522:67 V1 | 1885 | testdata/Builtins.lc 522:35-522:71 V1 |
1896 | testdata/Builtins.lc 522:51-522:56 Type | 1886 | testdata/Builtins.lc 522:51-522:56 Type |
1897 | testdata/Builtins.lc 522:1-522:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1887 | testdata/Builtins.lc 522:66-522:71 Type |
1898 | testdata/Builtins.lc 523:35-523:77 Type | 1888 | testdata/Builtins.lc 522:1-522:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float |
1899 | testdata/Builtins.lc 523:35-523:77 V3 | 1889 | testdata/Builtins.lc 523:35-523:76 Type |
1890 | testdata/Builtins.lc 523:35-523:76 V3 | ||
1900 | testdata/Builtins.lc 523:39-523:48 'Nat -> Type->Type | 1891 | testdata/Builtins.lc 523:39-523:48 'Nat -> Type->Type |
1901 | testdata/Builtins.lc 523:35-523:77 'Nat | 1892 | testdata/Builtins.lc 523:35-523:76 'Nat |
1902 | testdata/Builtins.lc 523:35-523:77 V1 | 1893 | testdata/Builtins.lc 523:35-523:76 V1 |
1903 | testdata/Builtins.lc 523:51-523:56 Type | 1894 | testdata/Builtins.lc 523:51-523:56 Type |
1904 | testdata/Builtins.lc 523:1-523:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a | 1895 | testdata/Builtins.lc 523:71-523:76 Type |
1905 | testdata/Builtins.lc 523:18-523:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a | 1896 | testdata/Builtins.lc 523:1-523:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float |
1897 | testdata/Builtins.lc 523:15-523:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float | ||
1906 | testdata/Builtins.lc 524:35-524:72 Type | 1898 | testdata/Builtins.lc 524:35-524:72 Type |
1907 | testdata/Builtins.lc 524:35-524:72 V3 | ||
1908 | testdata/Builtins.lc 524:39-524:48 'Nat -> Type->Type | ||
1909 | testdata/Builtins.lc 524:35-524:72 'Nat | ||
1910 | testdata/Builtins.lc 524:35-524:72 V1 | 1899 | testdata/Builtins.lc 524:35-524:72 V1 |
1900 | testdata/Builtins.lc 524:39-524:56 Type | ||
1901 | testdata/Builtins.lc 524:39-524:48 'Nat -> Type->Type | ||
1911 | testdata/Builtins.lc 524:51-524:56 Type | 1902 | testdata/Builtins.lc 524:51-524:56 Type |
1912 | testdata/Builtins.lc 524:1-524:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a | 1903 | testdata/Builtins.lc 524:1-524:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a |
1913 | testdata/Builtins.lc 526:34-526:56 Type | 1904 | testdata/Builtins.lc 525:35-525:67 Type |
1914 | testdata/Builtins.lc 526:34-526:37 'Nat -> 'Nat -> Type->Type | 1905 | testdata/Builtins.lc 525:35-525:67 V3 |
1915 | testdata/Builtins.lc 526:34-526:56 'Nat | 1906 | testdata/Builtins.lc 525:39-525:48 'Nat -> Type->Type |
1916 | testdata/Builtins.lc 526:34-526:56 V5 | 1907 | testdata/Builtins.lc 525:35-525:67 'Nat |
1917 | testdata/Builtins.lc 526:34-526:56 V3 | 1908 | testdata/Builtins.lc 525:35-525:67 V1 |
1918 | testdata/Builtins.lc 526:34-526:56 V1 | 1909 | testdata/Builtins.lc 525:51-525:56 Type |
1919 | testdata/Builtins.lc 526:47-526:50 'Nat -> 'Nat -> Type->Type | 1910 | testdata/Builtins.lc 525:1-525:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
1920 | testdata/Builtins.lc 526:1-526:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Mat b a c | 1911 | testdata/Builtins.lc 526:35-526:77 Type |
1921 | testdata/Builtins.lc 527:34-527:52 Type | 1912 | testdata/Builtins.lc 526:35-526:77 V3 |
1922 | testdata/Builtins.lc 527:34-527:37 'Nat -> 'Nat -> Type->Type | 1913 | testdata/Builtins.lc 526:39-526:48 'Nat -> Type->Type |
1923 | testdata/Builtins.lc 527:34-527:52 'Nat | 1914 | testdata/Builtins.lc 526:35-526:77 'Nat |
1924 | testdata/Builtins.lc 527:34-527:52 V3 | 1915 | testdata/Builtins.lc 526:35-526:77 V1 |
1925 | testdata/Builtins.lc 527:34-527:52 V1 | 1916 | testdata/Builtins.lc 526:51-526:56 Type |
1926 | testdata/Builtins.lc 527:47-527:52 Type | 1917 | testdata/Builtins.lc 526:1-526:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a |
1927 | testdata/Builtins.lc 527:1-527:16 {a:'Nat} -> {b} -> 'Mat a a b -> 'Float | 1918 | testdata/Builtins.lc 526:18-526:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a |
1928 | testdata/Builtins.lc 528:34-528:56 Type | 1919 | testdata/Builtins.lc 527:35-527:72 Type |
1929 | testdata/Builtins.lc 528:34-528:37 'Nat -> 'Nat -> Type->Type | 1920 | testdata/Builtins.lc 527:35-527:72 V3 |
1930 | testdata/Builtins.lc 528:34-528:56 'Nat | 1921 | testdata/Builtins.lc 527:39-527:48 'Nat -> Type->Type |
1931 | testdata/Builtins.lc 528:34-528:56 V3 | 1922 | testdata/Builtins.lc 527:35-527:72 'Nat |
1932 | testdata/Builtins.lc 528:34-528:56 V1 | 1923 | testdata/Builtins.lc 527:35-527:72 V1 |
1933 | testdata/Builtins.lc 528:47-528:50 'Nat -> 'Nat -> Type->Type | 1924 | testdata/Builtins.lc 527:51-527:56 Type |
1934 | testdata/Builtins.lc 528:1-528:12 {a:'Nat} -> {b} -> 'Mat a a b -> 'Mat a a b | 1925 | testdata/Builtins.lc 527:1-527:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a |
1935 | testdata/Builtins.lc 529:34-529:69 Type | 1926 | testdata/Builtins.lc 529:34-529:56 Type |
1936 | testdata/Builtins.lc 529:34-529:37 'Nat -> Type->Type | 1927 | testdata/Builtins.lc 529:34-529:37 'Nat -> 'Nat -> Type->Type |
1937 | testdata/Builtins.lc 529:34-529:69 'Nat | 1928 | testdata/Builtins.lc 529:34-529:56 'Nat |
1938 | testdata/Builtins.lc 529:34-529:69 V5 | 1929 | testdata/Builtins.lc 529:34-529:56 V5 |
1939 | testdata/Builtins.lc 529:34-529:69 V3 | 1930 | testdata/Builtins.lc 529:34-529:56 V3 |
1940 | testdata/Builtins.lc 529:47-529:50 'Nat -> Type->Type | 1931 | testdata/Builtins.lc 529:34-529:56 V1 |
1941 | testdata/Builtins.lc 529:34-529:69 V2 | 1932 | testdata/Builtins.lc 529:47-529:50 'Nat -> 'Nat -> Type->Type |
1942 | testdata/Builtins.lc 529:60-529:63 'Nat -> 'Nat -> Type->Type | 1933 | testdata/Builtins.lc 529:1-529:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Mat b a c |
1943 | testdata/Builtins.lc 529:1-529:17 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'VecS b c -> 'Mat c a b | 1934 | testdata/Builtins.lc 530:34-530:52 Type |
1944 | testdata/Builtins.lc 530:34-530:67 Type | ||
1945 | testdata/Builtins.lc 530:34-530:37 'Nat -> 'Nat -> Type->Type | 1935 | testdata/Builtins.lc 530:34-530:37 'Nat -> 'Nat -> Type->Type |
1946 | testdata/Builtins.lc 530:34-530:67 'Nat | 1936 | testdata/Builtins.lc 530:34-530:52 'Nat |
1947 | testdata/Builtins.lc 530:34-530:67 V5 | 1937 | testdata/Builtins.lc 530:34-530:52 V3 |
1948 | testdata/Builtins.lc 530:34-530:67 V3 | 1938 | testdata/Builtins.lc 530:34-530:52 V1 |
1949 | testdata/Builtins.lc 530:34-530:67 V1 | 1939 | testdata/Builtins.lc 530:47-530:52 Type |
1950 | testdata/Builtins.lc 530:47-530:50 'Nat -> Type->Type | 1940 | testdata/Builtins.lc 530:1-530:16 {a:'Nat} -> {b} -> 'Mat a a b -> 'Float |
1951 | testdata/Builtins.lc 530:60-530:63 'Nat -> Type->Type | 1941 | testdata/Builtins.lc 531:34-531:56 Type |
1952 | testdata/Builtins.lc 530:1-530:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'VecS c b -> 'VecS c a | 1942 | testdata/Builtins.lc 531:34-531:37 'Nat -> 'Nat -> Type->Type |
1953 | testdata/Builtins.lc 531:34-531:67 Type | 1943 | testdata/Builtins.lc 531:34-531:56 'Nat |
1954 | testdata/Builtins.lc 531:34-531:37 'Nat -> Type->Type | 1944 | testdata/Builtins.lc 531:34-531:56 V3 |
1955 | testdata/Builtins.lc 531:34-531:67 'Nat | 1945 | testdata/Builtins.lc 531:34-531:56 V1 |
1956 | testdata/Builtins.lc 531:34-531:67 V5 | ||
1957 | testdata/Builtins.lc 531:34-531:67 V3 | ||
1958 | testdata/Builtins.lc 531:47-531:50 'Nat -> 'Nat -> Type->Type | 1946 | testdata/Builtins.lc 531:47-531:50 'Nat -> 'Nat -> Type->Type |
1959 | testdata/Builtins.lc 531:34-531:67 V2 | 1947 | testdata/Builtins.lc 531:1-531:12 {a:'Nat} -> {b} -> 'Mat a a b -> 'Mat a a b |
1960 | testdata/Builtins.lc 531:60-531:63 'Nat -> Type->Type | ||
1961 | testdata/Builtins.lc 531:1-531:14 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'Mat a c b -> 'VecS b c | ||
1962 | testdata/Builtins.lc 532:34-532:69 Type | 1948 | testdata/Builtins.lc 532:34-532:69 Type |
1963 | testdata/Builtins.lc 532:34-532:37 'Nat -> 'Nat -> Type->Type | 1949 | testdata/Builtins.lc 532:34-532:37 'Nat -> Type->Type |
1964 | testdata/Builtins.lc 532:34-532:69 'Nat | 1950 | testdata/Builtins.lc 532:34-532:69 'Nat |
1965 | testdata/Builtins.lc 532:34-532:69 V7 | ||
1966 | testdata/Builtins.lc 532:34-532:69 V5 | 1951 | testdata/Builtins.lc 532:34-532:69 V5 |
1967 | testdata/Builtins.lc 532:34-532:69 V3 | 1952 | testdata/Builtins.lc 532:34-532:69 V3 |
1968 | testdata/Builtins.lc 532:47-532:50 'Nat -> 'Nat -> Type->Type | 1953 | testdata/Builtins.lc 532:47-532:50 'Nat -> Type->Type |
1969 | testdata/Builtins.lc 532:34-532:69 V2 | 1954 | testdata/Builtins.lc 532:34-532:69 V2 |
1970 | testdata/Builtins.lc 532:60-532:63 'Nat -> 'Nat -> Type->Type | 1955 | testdata/Builtins.lc 532:60-532:63 'Nat -> 'Nat -> Type->Type |
1971 | testdata/Builtins.lc 532:1-532:14 {a:'Nat} -> {b:'Nat} -> {c} -> {d:'Nat} -> 'Mat a b c -> 'Mat b d c -> 'Mat a d c | 1956 | testdata/Builtins.lc 532:1-532:17 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'VecS b c -> 'Mat c a b |
1972 | testdata/Builtins.lc 535:35-535:97 Type | 1957 | testdata/Builtins.lc 533:34-533:67 Type |
1973 | testdata/Builtins.lc 535:35-535:38 Type->Type | 1958 | testdata/Builtins.lc 533:34-533:37 'Nat -> 'Nat -> Type->Type |
1974 | testdata/Builtins.lc 535:35-535:97 V7 | 1959 | testdata/Builtins.lc 533:34-533:67 'Nat |
1975 | testdata/Builtins.lc 535:35-535:97 V6 | 1960 | testdata/Builtins.lc 533:34-533:67 V5 |
1976 | testdata/Builtins.lc 535:46-535:55 'Nat -> Type->Type | 1961 | testdata/Builtins.lc 533:34-533:67 V3 |
1977 | testdata/Builtins.lc 535:35-535:97 'Nat | 1962 | testdata/Builtins.lc 533:34-533:67 V1 |
1978 | testdata/Builtins.lc 535:35-535:97 V4 | 1963 | testdata/Builtins.lc 533:47-533:50 'Nat -> Type->Type |
1979 | testdata/Builtins.lc 535:35-535:97 V3 | 1964 | testdata/Builtins.lc 533:60-533:63 'Nat -> Type->Type |
1980 | testdata/Builtins.lc 535:65-535:74 'Nat -> Type->Type | 1965 | testdata/Builtins.lc 533:1-533:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'VecS c b -> 'VecS c a |
1981 | testdata/Builtins.lc 535:77-535:81 Type | 1966 | testdata/Builtins.lc 534:34-534:67 Type |
1982 | testdata/Builtins.lc 534:1-534:13 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1967 | testdata/Builtins.lc 534:34-534:37 'Nat -> Type->Type |
1983 | testdata/Builtins.lc 534:15-534:32 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1968 | testdata/Builtins.lc 534:34-534:67 'Nat |
1984 | testdata/Builtins.lc 534:34-534:49 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1969 | testdata/Builtins.lc 534:34-534:67 V5 |
1985 | testdata/Builtins.lc 534:51-534:71 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1970 | testdata/Builtins.lc 534:34-534:67 V3 |
1986 | testdata/Builtins.lc 534:73-534:83 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1971 | testdata/Builtins.lc 534:47-534:50 'Nat -> 'Nat -> Type->Type |
1987 | testdata/Builtins.lc 534:85-534:98 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d | 1972 | testdata/Builtins.lc 534:34-534:67 V2 |
1988 | testdata/Builtins.lc 536:35-536:76 Type | 1973 | testdata/Builtins.lc 534:60-534:63 'Nat -> Type->Type |
1989 | testdata/Builtins.lc 536:35-536:76 V3 | 1974 | testdata/Builtins.lc 534:1-534:14 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'Mat a c b -> 'VecS b c |
1990 | testdata/Builtins.lc 536:39-536:55 Type->Type | 1975 | testdata/Builtins.lc 535:34-535:69 Type |
1991 | testdata/Builtins.lc 536:35-536:76 V1 | 1976 | testdata/Builtins.lc 535:34-535:37 'Nat -> 'Nat -> Type->Type |
1992 | testdata/Builtins.lc 536:72-536:76 Type | 1977 | testdata/Builtins.lc 535:34-535:69 'Nat |
1993 | testdata/Builtins.lc 536:1-536:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool | 1978 | testdata/Builtins.lc 535:34-535:69 V7 |
1994 | testdata/Builtins.lc 536:12-536:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool | 1979 | testdata/Builtins.lc 535:34-535:69 V5 |
1995 | testdata/Builtins.lc 539:35-539:67 Type | 1980 | testdata/Builtins.lc 535:34-535:69 V3 |
1996 | testdata/Builtins.lc 539:35-539:67 V3 | 1981 | testdata/Builtins.lc 535:47-535:50 'Nat -> 'Nat -> Type->Type |
1997 | testdata/Builtins.lc 539:39-539:48 'Nat -> Type->Type | 1982 | testdata/Builtins.lc 535:34-535:69 V2 |
1998 | testdata/Builtins.lc 539:35-539:67 'Nat | 1983 | testdata/Builtins.lc 535:60-535:63 'Nat -> 'Nat -> Type->Type |
1999 | testdata/Builtins.lc 539:35-539:67 V1 | 1984 | testdata/Builtins.lc 535:1-535:14 {a:'Nat} -> {b:'Nat} -> {c} -> {d:'Nat} -> 'Mat a b c -> 'Mat b d c -> 'Mat a d c |
2000 | testdata/Builtins.lc 539:51-539:56 Type | 1985 | testdata/Builtins.lc 538:35-538:97 Type |
2001 | testdata/Builtins.lc 538:1-538:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1986 | testdata/Builtins.lc 538:35-538:38 Type->Type |
2002 | testdata/Builtins.lc 538:11-538:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1987 | testdata/Builtins.lc 538:35-538:97 V7 |
2003 | testdata/Builtins.lc 538:21-538:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | 1988 | testdata/Builtins.lc 538:35-538:97 V6 |
2004 | testdata/Builtins.lc 541:34-541:60 Type | 1989 | testdata/Builtins.lc 538:46-538:55 'Nat -> Type->Type |
2005 | testdata/Builtins.lc 541:34-541:43 'Nat -> Type->Type | 1990 | testdata/Builtins.lc 538:35-538:97 'Nat |
2006 | testdata/Builtins.lc 541:34-541:60 'Nat | 1991 | testdata/Builtins.lc 538:35-538:97 V4 |
2007 | testdata/Builtins.lc 541:34-541:60 V1 | 1992 | testdata/Builtins.lc 538:35-538:97 V3 |
2008 | testdata/Builtins.lc 541:46-541:51 Type | 1993 | testdata/Builtins.lc 538:65-538:74 'Nat -> Type->Type |
2009 | testdata/Builtins.lc 541:55-541:60 Type | 1994 | testdata/Builtins.lc 538:77-538:81 Type |
2010 | testdata/Builtins.lc 541:1-541:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float | 1995 | testdata/Builtins.lc 537:1-537:13 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2011 | testdata/Builtins.lc 542:34-542:66 Type | 1996 | testdata/Builtins.lc 537:15-537:32 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2012 | testdata/Builtins.lc 542:34-542:43 'Nat -> Type->Type | 1997 | testdata/Builtins.lc 537:34-537:49 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2013 | testdata/Builtins.lc 542:34-542:66 'Nat | 1998 | testdata/Builtins.lc 537:51-537:71 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2014 | testdata/Builtins.lc 542:34-542:66 V1 | 1999 | testdata/Builtins.lc 537:73-537:83 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2015 | testdata/Builtins.lc 542:46-542:51 Type | 2000 | testdata/Builtins.lc 537:85-537:98 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d |
2016 | testdata/Builtins.lc 542:55-542:66 Type | 2001 | testdata/Builtins.lc 539:35-539:76 Type |
2017 | testdata/Builtins.lc 542:55-542:58 'Nat -> Type->Type | 2002 | testdata/Builtins.lc 539:35-539:76 V3 |
2018 | testdata/Builtins.lc 542:61-542:66 Type | 2003 | testdata/Builtins.lc 539:39-539:55 Type->Type |
2019 | testdata/Builtins.lc 542:1-542:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) | 2004 | testdata/Builtins.lc 539:35-539:76 V1 |
2020 | testdata/Builtins.lc 543:34-543:66 Type | 2005 | testdata/Builtins.lc 539:72-539:76 Type |
2021 | testdata/Builtins.lc 543:34-543:43 'Nat -> Type->Type | 2006 | testdata/Builtins.lc 539:1-539:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool |
2022 | testdata/Builtins.lc 543:34-543:66 'Nat | 2007 | testdata/Builtins.lc 539:12-539:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool |
2023 | testdata/Builtins.lc 543:34-543:66 V1 | 2008 | testdata/Builtins.lc 542:35-542:67 Type |
2024 | testdata/Builtins.lc 543:46-543:51 Type | 2009 | testdata/Builtins.lc 542:35-542:67 V3 |
2025 | testdata/Builtins.lc 543:55-543:66 Type | 2010 | testdata/Builtins.lc 542:39-542:48 'Nat -> Type->Type |
2026 | testdata/Builtins.lc 543:55-543:58 'Nat -> Type->Type | 2011 | testdata/Builtins.lc 542:35-542:67 'Nat |
2027 | testdata/Builtins.lc 543:61-543:66 Type | 2012 | testdata/Builtins.lc 542:35-542:67 V1 |
2028 | testdata/Builtins.lc 543:1-543:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) | 2013 | testdata/Builtins.lc 542:51-542:56 Type |
2029 | testdata/Builtins.lc 544:34-544:66 Type | 2014 | testdata/Builtins.lc 541:1-541:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a |
2015 | testdata/Builtins.lc 541:11-541:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
2016 | testdata/Builtins.lc 541:21-541:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a | ||
2017 | testdata/Builtins.lc 544:34-544:60 Type | ||
2030 | testdata/Builtins.lc 544:34-544:43 'Nat -> Type->Type | 2018 | testdata/Builtins.lc 544:34-544:43 'Nat -> Type->Type |
2031 | testdata/Builtins.lc 544:34-544:66 'Nat | 2019 | testdata/Builtins.lc 544:34-544:60 'Nat |
2032 | testdata/Builtins.lc 544:34-544:66 V1 | 2020 | testdata/Builtins.lc 544:34-544:60 V1 |
2033 | testdata/Builtins.lc 544:46-544:51 Type | 2021 | testdata/Builtins.lc 544:46-544:51 Type |
2034 | testdata/Builtins.lc 544:55-544:66 Type | 2022 | testdata/Builtins.lc 544:55-544:60 Type |
2035 | testdata/Builtins.lc 544:55-544:58 'Nat -> Type->Type | 2023 | testdata/Builtins.lc 544:1-544:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float |
2036 | testdata/Builtins.lc 544:61-544:66 Type | 2024 | testdata/Builtins.lc 545:34-545:66 Type |
2037 | testdata/Builtins.lc 544:1-544:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) | 2025 | testdata/Builtins.lc 545:34-545:43 'Nat -> Type->Type |
2038 | testdata/Builtins.lc 560:6-560:13 Type | 2026 | testdata/Builtins.lc 545:34-545:66 'Nat |
2039 | testdata/Builtins.lc 561:20-561:26 Type | 2027 | testdata/Builtins.lc 545:34-545:66 V1 |
2040 | testdata/Builtins.lc 562:20-562:27 Type | 2028 | testdata/Builtins.lc 545:46-545:51 Type |
2041 | testdata/Builtins.lc 561:3-561:16 'String->'Texture | 2029 | testdata/Builtins.lc 545:55-545:66 Type |
2042 | testdata/Builtins.lc 564:20-564:23 'Nat -> Type->Type | 2030 | testdata/Builtins.lc 545:55-545:58 'Nat -> Type->Type |
2043 | testdata/Builtins.lc 564:26-564:29 Type | 2031 | testdata/Builtins.lc 545:61-545:66 Type |
2044 | testdata/Builtins.lc 565:20-566:27 Type | 2032 | testdata/Builtins.lc 545:1-545:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) |
2045 | testdata/Builtins.lc 565:20-565:25 'Nat -> Type->Type | 2033 | testdata/Builtins.lc 546:34-546:66 Type |
2046 | testdata/Builtins.lc 565:29-565:47 Type | 2034 | testdata/Builtins.lc 546:34-546:43 'Nat -> Type->Type |
2047 | testdata/Builtins.lc 565:29-565:34 Type->Type | 2035 | testdata/Builtins.lc 546:34-546:66 'Nat |
2048 | testdata/Builtins.lc 565:36-565:47 Type | 2036 | testdata/Builtins.lc 546:34-546:66 V1 |
2049 | testdata/Builtins.lc 565:36-565:39 'Nat -> Type->Type | 2037 | testdata/Builtins.lc 546:46-546:51 Type |
2050 | testdata/Builtins.lc 565:42-565:47 Type | 2038 | testdata/Builtins.lc 546:55-546:66 Type |
2051 | testdata/Builtins.lc 566:20-566:27 Type | 2039 | testdata/Builtins.lc 546:55-546:58 'Nat -> Type->Type |
2052 | testdata/Builtins.lc 564:3-564:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture | 2040 | testdata/Builtins.lc 546:61-546:66 Type |
2053 | testdata/Builtins.lc 568:6-568:12 Type | 2041 | testdata/Builtins.lc 546:1-546:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) |
2054 | testdata/Builtins.lc 569:5-569:16 'Filter | 2042 | testdata/Builtins.lc 547:34-547:66 Type |
2055 | testdata/Builtins.lc 570:5-570:17 'Filter | 2043 | testdata/Builtins.lc 547:34-547:43 'Nat -> Type->Type |
2056 | testdata/Builtins.lc 572:6-572:14 Type | 2044 | testdata/Builtins.lc 547:34-547:66 'Nat |
2057 | testdata/Builtins.lc 573:5-573:11 'EdgeMode | 2045 | testdata/Builtins.lc 547:34-547:66 V1 |
2058 | testdata/Builtins.lc 574:5-574:19 'EdgeMode | 2046 | testdata/Builtins.lc 547:46-547:51 Type |
2059 | testdata/Builtins.lc 575:5-575:16 'EdgeMode | 2047 | testdata/Builtins.lc 547:55-547:66 Type |
2060 | testdata/Builtins.lc 577:6-577:13 Type | 2048 | testdata/Builtins.lc 547:55-547:58 'Nat -> Type->Type |
2061 | testdata/Builtins.lc 577:24-577:30 Type | 2049 | testdata/Builtins.lc 547:61-547:66 Type |
2062 | testdata/Builtins.lc 577:6-577:47 Type | 2050 | testdata/Builtins.lc 547:1-547:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) |
2063 | testdata/Builtins.lc 577:31-577:39 Type | 2051 | testdata/Builtins.lc 563:6-563:13 Type |
2064 | testdata/Builtins.lc 577:40-577:47 Type | 2052 | testdata/Builtins.lc 564:20-564:26 Type |
2065 | testdata/Builtins.lc 577:16-577:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler | 2053 | testdata/Builtins.lc 565:20-565:27 Type |
2066 | testdata/Builtins.lc 580:14-580:21 Type | 2054 | testdata/Builtins.lc 564:3-564:16 'String->'Texture |
2067 | testdata/Builtins.lc 580:25-580:51 Type | 2055 | testdata/Builtins.lc 567:20-567:23 'Nat -> Type->Type |
2068 | testdata/Builtins.lc 580:25-580:28 'Nat -> Type->Type | 2056 | testdata/Builtins.lc 567:26-567:29 Type |
2069 | testdata/Builtins.lc 580:31-580:36 Type | 2057 | testdata/Builtins.lc 568:20-569:27 Type |
2070 | testdata/Builtins.lc 580:40-580:51 Type | 2058 | testdata/Builtins.lc 568:20-568:25 'Nat -> Type->Type |
2071 | testdata/Builtins.lc 580:40-580:43 'Nat -> Type->Type | 2059 | testdata/Builtins.lc 568:29-568:47 Type |
2072 | testdata/Builtins.lc 580:46-580:51 Type | 2060 | testdata/Builtins.lc 568:29-568:34 Type->Type |
2073 | testdata/Builtins.lc 580:1-580:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) | 2061 | testdata/Builtins.lc 568:36-568:47 Type |
2074 | testdata/Builtins.lc 583:30-583:39 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 2062 | testdata/Builtins.lc 568:36-568:39 'Nat -> Type->Type |
2075 | testdata/Builtins.lc 583:41-583:60 V1->V1 | 2063 | testdata/Builtins.lc 568:42-568:47 Type |
2076 | testdata/Builtins.lc 583:41-583:51 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Fragment (Succ Zero) DefinedDepth a | 2064 | testdata/Builtins.lc 569:20-569:27 Type |
2077 | testdata/Builtins.lc 583:53-583:60 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float | 2065 | testdata/Builtins.lc 567:3-567:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture |
2078 | testdata/Builtins.lc 583:59-583:60 'Float | 2066 | testdata/Builtins.lc 571:6-571:12 Type |
2079 | testdata/Builtins.lc 583:59-583:60 'Int | 2067 | testdata/Builtins.lc 572:5-572:16 'Filter |
2080 | testdata/Builtins.lc 583:1-583:20 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) | 2068 | testdata/Builtins.lc 573:5-573:17 'Filter |
2081 | testdata/Builtins.lc 584:46-584:55 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b | 2069 | testdata/Builtins.lc 575:6-575:14 Type |
2082 | testdata/Builtins.lc 584:57-584:67 V1->V1 | 2070 | testdata/Builtins.lc 576:5-576:11 'EdgeMode |
2083 | testdata/Builtins.lc 584:57-584:67 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Fragment (Succ Zero) DefinedDepth a | 2071 | testdata/Builtins.lc 577:5-577:19 'EdgeMode |
2084 | testdata/Builtins.lc 584:1-584:33 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a) -> 'Float) -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) | 2072 | testdata/Builtins.lc 578:5-578:16 'EdgeMode |
2085 | testdata/Builtins.lc 585:24-585:32 {a} -> {b} -> a -> b -> 'Tuple2 a b | 2073 | testdata/Builtins.lc 580:6-580:13 Type |
2086 | testdata/Builtins.lc 585:1-585:15 {a} -> {b} -> a -> b -> 'Tuple2 a b | 2074 | testdata/Builtins.lc 580:24-580:30 Type |
2087 | testdata/Builtins.lc 586:25-586:35 V2 -> V2->V2 | 2075 | testdata/Builtins.lc 580:6-580:47 Type |
2088 | testdata/Builtins.lc 586:25-586:35 V2->V2 | 2076 | testdata/Builtins.lc 580:31-580:39 Type |
2089 | testdata/Builtins.lc 586:25-586:35 V2 | 2077 | testdata/Builtins.lc 580:40-580:47 Type |
2090 | testdata/Builtins.lc 586:25-586:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b | 2078 | testdata/Builtins.lc 580:16-580:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler |
2091 | testdata/Builtins.lc 586:13-586:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) | 2079 | testdata/Builtins.lc 583:14-583:21 Type |
2092 | testdata/Builtins.lc 586:13-586:21 V4 | 2080 | testdata/Builtins.lc 583:25-583:51 Type |
2093 | testdata/Builtins.lc 586:1-586:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b | 2081 | testdata/Builtins.lc 583:25-583:28 'Nat -> Type->Type |
2094 | testdata/Builtins.lc 587:15-587:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output | 2082 | testdata/Builtins.lc 583:31-583:36 Type |
2095 | testdata/Builtins.lc 587:1-587:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output | 2083 | testdata/Builtins.lc 583:40-583:51 Type |
2096 | testdata/Builtins.lc 588:14-588:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b | 2084 | testdata/Builtins.lc 583:40-583:43 'Nat -> Type->Type |
2097 | testdata/Builtins.lc 588:1-588:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b | 2085 | testdata/Builtins.lc 583:46-583:51 Type |
2098 | testdata/Builtins.lc 589:19-589:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) | 2086 | testdata/Builtins.lc 583:1-583:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) |
2099 | testdata/Builtins.lc 589:1-589:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) | 2087 | testdata/Builtins.lc 586:30-586:45 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b |
2100 | testdata/Builtins.lc 590:19-590:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) | 2088 | testdata/Builtins.lc 586:47-586:66 V1 -> 'Stream V1 |
2101 | testdata/Builtins.lc 590:1-590:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c) | 2089 | testdata/Builtins.lc 586:47-586:57 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) |
2090 | testdata/Builtins.lc 586:59-586:66 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float | ||
2091 | testdata/Builtins.lc 586:65-586:66 'Float | ||
2092 | testdata/Builtins.lc 586:65-586:66 'Int | ||
2093 | testdata/Builtins.lc 586:1-586:20 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) | ||
2094 | testdata/Builtins.lc 587:46-587:61 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b | ||
2095 | testdata/Builtins.lc 587:63-587:73 V1 -> 'Stream V1 | ||
2096 | testdata/Builtins.lc 587:63-587:73 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) | ||
2097 | testdata/Builtins.lc 587:1-587:33 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a) -> 'Float) -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) | ||
2098 | testdata/Builtins.lc 588:24-588:32 {a} -> {b} -> a -> b -> 'Tuple2 a b | ||
2099 | testdata/Builtins.lc 588:1-588:15 {a} -> {b} -> a -> b -> 'Tuple2 a b | ||
2100 | testdata/Builtins.lc 589:25-589:35 V2 -> V2->V2 | ||
2101 | testdata/Builtins.lc 589:25-589:35 V2->V2 | ||
2102 | testdata/Builtins.lc 589:25-589:35 V2 | ||
2103 | testdata/Builtins.lc 589:25-589:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b | ||
2104 | testdata/Builtins.lc 589:13-589:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) | ||
2105 | testdata/Builtins.lc 589:13-589:21 V4 | ||
2106 | testdata/Builtins.lc 589:1-589:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b | ||
2107 | testdata/Builtins.lc 590:15-590:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output | ||
2108 | testdata/Builtins.lc 590:1-590:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output | ||
2109 | testdata/Builtins.lc 591:14-591:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b | ||
2110 | testdata/Builtins.lc 591:1-591:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b | ||
2111 | testdata/Builtins.lc 592:19-592:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) | ||
2112 | testdata/Builtins.lc 592:1-592:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) | ||
2113 | testdata/Builtins.lc 593:19-593:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) | ||
2114 | testdata/Builtins.lc 593:1-593:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c) | ||