main is not found tooltips: testdata/Builtins.lc 9:1-9:3 {a} -> a->a testdata/Builtins.lc 13:6-13:9 Type testdata/Builtins.lc 13:12-13:16 'Nat testdata/Builtins.lc 13:24-13:27 Type testdata/Builtins.lc 13:19-13:23 'Nat->'Nat testdata/Builtins.lc 15:6-15:10 Type->Type testdata/Builtins.lc 15:6-15:10 Type testdata/Builtins.lc 15:15-15:18 {a} -> 'List a testdata/Builtins.lc 15:6-15:35 Type testdata/Builtins.lc 15:26-15:27 Type testdata/Builtins.lc 15:29-15:33 Type->Type testdata/Builtins.lc 15:34-15:35 Type testdata/Builtins.lc 15:21-15:25 {a} -> a -> 'List a -> 'List a testdata/Builtins.lc 20:22-23:31 Type -> Type->Type testdata/Builtins.lc 20:22-23:31 Type->Type testdata/Builtins.lc 20:22-23:31 Type testdata/Builtins.lc 20:30-20:39 Type -> Type->Type testdata/Builtins.lc 20:30-20:39 Type->Type testdata/Builtins.lc 20:30-20:39 Type testdata/Builtins.lc 20:30-20:39 Type -> Type -> Type->Type testdata/Builtins.lc 20:22-20:26 Type testdata/Builtins.lc 21:22-23:31 Type testdata/Builtins.lc 21:33-21:45 Type -> Type -> Type->Type testdata/Builtins.lc 21:33-21:45 Type -> Type->Type testdata/Builtins.lc 21:33-21:45 Type->Type testdata/Builtins.lc 21:33-21:45 Type testdata/Builtins.lc 21:33-21:45 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 21:22-21:29 Type testdata/Builtins.lc 22:22-23:31 Type testdata/Builtins.lc 22:36-22:51 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 22:36-22:51 Type -> Type -> Type->Type testdata/Builtins.lc 22:36-22:51 Type -> Type->Type testdata/Builtins.lc 22:36-22:51 Type->Type testdata/Builtins.lc 22:36-22:51 Type testdata/Builtins.lc 22:36-22:51 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 22:22-22:32 Type testdata/Builtins.lc 23:25-23:31 Type testdata/Builtins.lc 23:25-23:31 Type -> Type->Type testdata/Builtins.lc 19:5-19:18 Type -> Type->Type testdata/Builtins.lc 26:10-26:24 V0->Type testdata/Builtins.lc 26:10-26:24 Type testdata/Builtins.lc 25:7-25:21 {a} -> a->Type testdata/Builtins.lc 28:10-28:21 V0->Type testdata/Builtins.lc 28:10-28:21 Type testdata/Builtins.lc 27:7-27:18 {a} -> a->Type testdata/Builtins.lc 30:10-30:26 V0->Type testdata/Builtins.lc 30:10-30:26 Type testdata/Builtins.lc 29:7-29:23 {a} -> a->Type testdata/Builtins.lc 32:17-32:21 Type testdata/Builtins.lc 32:26-32:37 Type testdata/Builtins.lc 32:26-32:29 Type testdata/Builtins.lc 32:33-32:37 Type testdata/Builtins.lc 32:6-32:10 Type -> 'Nat->Type testdata/Builtins.lc 33:9-33:25 Type testdata/Builtins.lc 33:9-33:10 Type testdata/Builtins.lc 33:14-33:25 Type testdata/Builtins.lc 33:14-33:15 Type testdata/Builtins.lc 33:19-33:25 Type testdata/Builtins.lc 33:19-33:23 Type -> 'Nat->Type testdata/Builtins.lc 33:24-33:25 Type testdata/Builtins.lc 33:3-33:5 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 34:9-34:30 Type testdata/Builtins.lc 34:9-34:10 Type testdata/Builtins.lc 34:14-34:30 Type testdata/Builtins.lc 34:14-34:15 Type testdata/Builtins.lc 34:19-34:30 Type testdata/Builtins.lc 34:19-34:20 Type testdata/Builtins.lc 34:24-34:30 Type testdata/Builtins.lc 34:24-34:28 Type -> 'Nat->Type testdata/Builtins.lc 34:29-34:30 Type testdata/Builtins.lc 34:3-34:5 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 35:9-35:35 Type testdata/Builtins.lc 35:9-35:10 Type testdata/Builtins.lc 35:14-35:35 Type testdata/Builtins.lc 35:14-35:15 Type testdata/Builtins.lc 35:19-35:35 Type testdata/Builtins.lc 35:19-35:20 Type testdata/Builtins.lc 35:24-35:35 Type testdata/Builtins.lc 35:24-35:25 Type testdata/Builtins.lc 35:29-35:35 Type testdata/Builtins.lc 35:29-35:33 Type -> 'Nat->Type testdata/Builtins.lc 35:34-35:35 Type testdata/Builtins.lc 35:3-35:5 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 37:23-37:26 Type testdata/Builtins.lc 37:47-37:51 'Nat -> Type->Type testdata/Builtins.lc 37:47-37:51 Type->Type testdata/Builtins.lc 37:47-37:51 Type testdata/Builtins.lc 37:47-37:51 Type -> 'Nat->Type testdata/Builtins.lc 37:37-37:40 'Nat -> Type->Type testdata/Builtins.lc 39:29-39:32 Type testdata/Builtins.lc 40:15-41:54 'Nat -> Type->Type testdata/Builtins.lc 40:15-41:54 Type->Type testdata/Builtins.lc 40:15-41:54 Type testdata/Builtins.lc 41:37-41:54 'Nat->Type testdata/Builtins.lc 41:37-41:54 Type testdata/Builtins.lc 41:37-41:40 'Nat -> Type->Type testdata/Builtins.lc 41:43-41:54 'Nat testdata/Builtins.lc 41:43-41:47 'Nat->'Nat testdata/Builtins.lc 41:50-41:54 'Nat testdata/Builtins.lc 41:50-41:54 'Nat->'Nat testdata/Builtins.lc 40:15-40:16 'Nat testdata/Builtins.lc 40:5-40:14 'Nat -> Type->Type testdata/Builtins.lc 44:25-44:28 Type testdata/Builtins.lc 45:17-45:20 'Nat -> Type->Type testdata/Builtins.lc 45:17-45:20 Type->Type testdata/Builtins.lc 45:17-45:20 Type testdata/Builtins.lc 45:5-45:10 'Nat -> Type->Type testdata/Builtins.lc 48:13-48:16 Type testdata/Builtins.lc 48:20-48:39 Type testdata/Builtins.lc 48:20-48:23 Type testdata/Builtins.lc 48:27-48:39 Type testdata/Builtins.lc 48:27-48:31 Type testdata/Builtins.lc 48:35-48:39 Type testdata/Builtins.lc 48:6-48:9 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 49:11-49:14 'Nat -> Type->Type testdata/Builtins.lc 49:17-49:22 Type testdata/Builtins.lc 49:26-49:54 Type testdata/Builtins.lc 49:26-49:29 'Nat -> Type->Type testdata/Builtins.lc 49:32-49:37 Type testdata/Builtins.lc 49:41-49:54 Type testdata/Builtins.lc 49:41-49:44 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 49:49-49:54 Type testdata/Builtins.lc 49:3-49:7 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'Mat (Succ (Succ Zero)) (Succ (Succ Zero)) 'Float testdata/Builtins.lc 50:11-50:14 'Nat -> Type->Type testdata/Builtins.lc 50:17-50:22 Type testdata/Builtins.lc 50:26-50:54 Type testdata/Builtins.lc 50:26-50:29 'Nat -> Type->Type testdata/Builtins.lc 50:32-50:37 Type testdata/Builtins.lc 50:41-50:54 Type testdata/Builtins.lc 50:41-50:44 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 50:49-50:54 Type testdata/Builtins.lc 50:3-50:7 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'Mat (Succ (Succ (Succ Zero))) (Succ (Succ Zero)) 'Float testdata/Builtins.lc 51:11-51:14 'Nat -> Type->Type testdata/Builtins.lc 51:17-51:22 Type testdata/Builtins.lc 51:26-51:54 Type testdata/Builtins.lc 51:26-51:29 'Nat -> Type->Type testdata/Builtins.lc 51:32-51:37 Type testdata/Builtins.lc 51:41-51:54 Type testdata/Builtins.lc 51:41-51:44 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 51:49-51:54 Type testdata/Builtins.lc 51:3-51:7 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ Zero)) 'Float testdata/Builtins.lc 52:11-52:14 'Nat -> Type->Type testdata/Builtins.lc 52:17-52:22 Type testdata/Builtins.lc 52:26-52:69 Type testdata/Builtins.lc 52:26-52:29 'Nat -> Type->Type testdata/Builtins.lc 52:32-52:37 Type testdata/Builtins.lc 52:41-52:69 Type testdata/Builtins.lc 52:41-52:44 'Nat -> Type->Type testdata/Builtins.lc 52:47-52:52 Type testdata/Builtins.lc 52:56-52:69 Type testdata/Builtins.lc 52:56-52:59 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 52:64-52:69 Type testdata/Builtins.lc 52:3-52:7 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'Mat (Succ (Succ Zero)) (Succ (Succ (Succ Zero))) 'Float testdata/Builtins.lc 53:11-53:14 'Nat -> Type->Type testdata/Builtins.lc 53:17-53:22 Type testdata/Builtins.lc 53:26-53:69 Type testdata/Builtins.lc 53:26-53:29 'Nat -> Type->Type testdata/Builtins.lc 53:32-53:37 Type testdata/Builtins.lc 53:41-53:69 Type testdata/Builtins.lc 53:41-53:44 'Nat -> Type->Type testdata/Builtins.lc 53:47-53:52 Type testdata/Builtins.lc 53:56-53:69 Type testdata/Builtins.lc 53:56-53:59 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 53:64-53:69 Type testdata/Builtins.lc 53:3-53:7 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'Mat (Succ (Succ (Succ Zero))) (Succ (Succ (Succ Zero))) 'Float testdata/Builtins.lc 54:11-54:14 'Nat -> Type->Type testdata/Builtins.lc 54:17-54:22 Type testdata/Builtins.lc 54:26-54:69 Type testdata/Builtins.lc 54:26-54:29 'Nat -> Type->Type testdata/Builtins.lc 54:32-54:37 Type testdata/Builtins.lc 54:41-54:69 Type testdata/Builtins.lc 54:41-54:44 'Nat -> Type->Type testdata/Builtins.lc 54:47-54:52 Type testdata/Builtins.lc 54:56-54:69 Type testdata/Builtins.lc 54:56-54:59 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 54:64-54:69 Type testdata/Builtins.lc 54:3-54:7 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) 'Float testdata/Builtins.lc 55:11-55:14 'Nat -> Type->Type testdata/Builtins.lc 55:17-55:22 Type testdata/Builtins.lc 55:26-55:84 Type testdata/Builtins.lc 55:26-55:29 'Nat -> Type->Type testdata/Builtins.lc 55:32-55:37 Type testdata/Builtins.lc 55:41-55:84 Type testdata/Builtins.lc 55:41-55:44 'Nat -> Type->Type testdata/Builtins.lc 55:47-55:52 Type testdata/Builtins.lc 55:56-55:84 Type testdata/Builtins.lc 55:56-55:59 'Nat -> Type->Type testdata/Builtins.lc 55:62-55:67 Type testdata/Builtins.lc 55:71-55:84 Type testdata/Builtins.lc 55:71-55:74 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 55:79-55:84 Type testdata/Builtins.lc 55:3-55:7 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'Mat (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero)))) 'Float testdata/Builtins.lc 56:11-56:14 'Nat -> Type->Type testdata/Builtins.lc 56:17-56:22 Type testdata/Builtins.lc 56:26-56:84 Type testdata/Builtins.lc 56:26-56:29 'Nat -> Type->Type testdata/Builtins.lc 56:32-56:37 Type testdata/Builtins.lc 56:41-56:84 Type testdata/Builtins.lc 56:41-56:44 'Nat -> Type->Type testdata/Builtins.lc 56:47-56:52 Type testdata/Builtins.lc 56:56-56:84 Type testdata/Builtins.lc 56:56-56:59 'Nat -> Type->Type testdata/Builtins.lc 56:62-56:67 Type testdata/Builtins.lc 56:71-56:84 Type testdata/Builtins.lc 56:71-56:74 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 56:79-56:84 Type testdata/Builtins.lc 56:3-56:7 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'Mat (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) 'Float testdata/Builtins.lc 57:11-57:14 'Nat -> Type->Type testdata/Builtins.lc 57:17-57:22 Type testdata/Builtins.lc 57:26-57:84 Type testdata/Builtins.lc 57:26-57:29 'Nat -> Type->Type testdata/Builtins.lc 57:32-57:37 Type testdata/Builtins.lc 57:41-57:84 Type testdata/Builtins.lc 57:41-57:44 'Nat -> Type->Type testdata/Builtins.lc 57:47-57:52 Type testdata/Builtins.lc 57:56-57:84 Type testdata/Builtins.lc 57:56-57:59 'Nat -> Type->Type testdata/Builtins.lc 57:62-57:67 Type testdata/Builtins.lc 57:71-57:84 Type testdata/Builtins.lc 57:71-57:74 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 57:79-57:84 Type testdata/Builtins.lc 57:3-57:7 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ (Succ Zero)))) 'Float testdata/Builtins.lc 49:49-57:84 Type testdata/Builtins.lc 50:49-57:84 Type testdata/Builtins.lc 51:49-57:84 Type testdata/Builtins.lc 52:64-57:84 Type testdata/Builtins.lc 53:64-57:84 Type testdata/Builtins.lc 54:64-57:84 Type testdata/Builtins.lc 55:79-57:84 Type testdata/Builtins.lc 56:79-57:84 Type testdata/Builtins.lc 60:22-64:32 Type->Type testdata/Builtins.lc 60:22-64:32 Type testdata/Builtins.lc 60:30-60:35 Type testdata/Builtins.lc 60:22-60:27 Type testdata/Builtins.lc 61:22-64:32 Type testdata/Builtins.lc 61:29-61:33 Type testdata/Builtins.lc 61:22-61:26 Type testdata/Builtins.lc 62:22-64:32 Type testdata/Builtins.lc 62:28-62:31 Type testdata/Builtins.lc 62:22-62:25 Type testdata/Builtins.lc 63:28-64:32 Type testdata/Builtins.lc 63:28-63:31 Type testdata/Builtins.lc 64:27-64:32 Type testdata/Builtins.lc 60:5-60:21 Type->Type testdata/Builtins.lc 68:17-68:52 Type -> Type->Type testdata/Builtins.lc 68:17-68:52 Type->Type testdata/Builtins.lc 68:17-68:52 Type testdata/Builtins.lc 68:28-68:52 Type -> 'Nat->Type testdata/Builtins.lc 68:28-68:52 'Nat->Type testdata/Builtins.lc 68:28-68:52 Type testdata/Builtins.lc 68:36-68:52 Type -> 'Nat->Type testdata/Builtins.lc 68:36-68:52 'Nat->Type testdata/Builtins.lc 68:36-68:52 Type testdata/Builtins.lc 68:36-68:38 Type -> Type->Type testdata/Builtins.lc 68:49-68:52 Type testdata/Builtins.lc 68:49-68:52 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 68:28-68:32 Type testdata/Builtins.lc 68:17-68:20 Type testdata/Builtins.lc 68:5-68:10 Type -> Type->Type testdata/Builtins.lc 72:6-72:11 Type testdata/Builtins.lc 72:14-72:16 'Swizz testdata/Builtins.lc 72:19-72:21 'Swizz testdata/Builtins.lc 72:24-72:26 'Swizz testdata/Builtins.lc 72:29-72:31 'Swizz testdata/Builtins.lc 75:27-75:56 Type testdata/Builtins.lc 75:27-75:28 V5 testdata/Builtins.lc 75:32-75:33 Type testdata/Builtins.lc 75:32-75:33 V4 testdata/Builtins.lc 75:38-75:56 Type testdata/Builtins.lc 75:38-75:41 'Nat -> Type->Type testdata/Builtins.lc 75:42-75:43 'Nat testdata/Builtins.lc 75:42-75:43 V2 testdata/Builtins.lc 75:44-75:45 Type testdata/Builtins.lc 75:49-75:56 Type testdata/Builtins.lc 75:49-75:52 'Nat -> Type->Type testdata/Builtins.lc 75:53-75:54 'Nat testdata/Builtins.lc 75:55-75:56 Type testdata/Builtins.lc 76:24-79:44 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 76:24-79:44 {a} -> {b:'Nat} -> V2->a -> 'VecS V3 b -> 'VecS a b testdata/Builtins.lc 76:24-79:44 {a:'Nat} -> V2->V2 -> 'VecS V3 a -> 'VecS V3 a testdata/Builtins.lc 76:24-79:44 V2->V2 -> 'VecS V3 V1 -> 'VecS V3 V2 testdata/Builtins.lc 76:24-79:44 'VecS V3 V1 -> 'VecS V3 V2 testdata/Builtins.lc 76:24-79:44 'VecS V3 V2 testdata/Builtins.lc 76:24-76:32 {a} -> (d : b:'Nat -> 'VecS a b -> Type) -> (e:a -> f:a -> d (Succ (Succ Zero)) (V2 a e f)) -> (h:a -> i:a -> j:a -> d (Succ (Succ (Succ Zero))) (V3 a h i j)) -> (l:a -> m:a -> n:a -> o:a -> d (Succ (Succ (Succ (Succ Zero)))) (V4 a l m n o)) -> {q:'Nat} -> (r : 'VecS a q) -> d q r testdata/Builtins.lc 76:34-76:50 a:'Nat -> 'VecS V1 a -> Type testdata/Builtins.lc 76:34-76:50 'VecS V1 V0 -> Type testdata/Builtins.lc 76:43-76:48 Type testdata/Builtins.lc 76:43-76:46 'Nat -> Type->Type testdata/Builtins.lc 76:47-76:48 'Nat testdata/Builtins.lc 77:6-77:28 V0 -> V1 -> 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 77:6-77:28 V1 -> 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 77:14-77:27 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 77:14-77:16 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 77:20-77:21 V0 testdata/Builtins.lc 77:20-77:21 V7 testdata/Builtins.lc 77:20-77:21 V2 testdata/Builtins.lc 77:26-77:27 V5 testdata/Builtins.lc 77:26-77:27 V6 testdata/Builtins.lc 78:6-78:36 V4 -> V5 -> V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 78:6-78:36 V5 -> V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 78:6-78:36 V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 78:16-78:35 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 78:16-78:18 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 78:22-78:23 V0 testdata/Builtins.lc 78:22-78:23 V7 testdata/Builtins.lc 78:28-78:29 V6 testdata/Builtins.lc 78:28-78:29 V7 testdata/Builtins.lc 78:34-78:35 V6 testdata/Builtins.lc 78:34-78:35 V7 testdata/Builtins.lc 79:6-79:44 V4 -> V5 -> V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:6-79:44 V5 -> V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:6-79:44 V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:6-79:44 V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:18-79:43 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:18-79:20 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 79:24-79:25 V0 testdata/Builtins.lc 79:24-79:25 V8 testdata/Builtins.lc 79:30-79:31 V7 testdata/Builtins.lc 79:30-79:31 V8 testdata/Builtins.lc 79:36-79:37 V7 testdata/Builtins.lc 79:36-79:37 V8 testdata/Builtins.lc 79:42-79:43 V7 testdata/Builtins.lc 79:42-79:43 V8 testdata/Builtins.lc 76:1-76:7 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 84:27-84:48 Type testdata/Builtins.lc 84:27-84:30 'Nat -> Type->Type testdata/Builtins.lc 84:31-84:32 'Nat testdata/Builtins.lc 84:31-84:32 V1 testdata/Builtins.lc 84:27-84:48 V2 testdata/Builtins.lc 84:38-84:43 Type testdata/Builtins.lc 85:17-90:28 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 85:17-90:28 {a:'Nat} -> 'VecS V1 a -> 'Swizz->V3 testdata/Builtins.lc 85:17-90:28 'VecS V1 V0 -> 'Swizz->V3 testdata/Builtins.lc 85:17-90:28 'Swizz->V3 testdata/Builtins.lc 85:17-90:28 V3 testdata/Builtins.lc 85:22-85:24 V1 -> V2->V2 testdata/Builtins.lc 85:22-85:24 V2->V2 testdata/Builtins.lc 85:22-85:24 V2 testdata/Builtins.lc 85:22-85:24 'Swizz testdata/Builtins.lc 87:24-87:26 V0 -> V1 -> V2->V3 testdata/Builtins.lc 87:24-87:26 V1 -> V2->V3 testdata/Builtins.lc 87:24-87:26 V2->V3 testdata/Builtins.lc 87:24-87:26 V3 testdata/Builtins.lc 87:24-87:26 'Swizz testdata/Builtins.lc 90:26-90:28 V0 -> V1 -> V2 -> V3->V4 testdata/Builtins.lc 90:26-90:28 V1 -> V2 -> V3->V4 testdata/Builtins.lc 90:26-90:28 V2 -> V3->V4 testdata/Builtins.lc 90:26-90:28 V3->V4 testdata/Builtins.lc 90:26-90:28 V4 testdata/Builtins.lc 90:26-90:28 'Swizz testdata/Builtins.lc 85:17-85:20 'VecS V1 V0 testdata/Builtins.lc 85:17-85:20 'VecS V5 V4 testdata/Builtins.lc 85:1-85:12 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 96:28-96:43 Type testdata/Builtins.lc 96:28-96:31 'Nat -> Type->Type testdata/Builtins.lc 96:32-96:33 'Nat testdata/Builtins.lc 96:32-96:33 V1 testdata/Builtins.lc 96:34-96:35 Type testdata/Builtins.lc 96:34-96:35 V2 testdata/Builtins.lc 96:39-96:43 Type testdata/Builtins.lc 97:16-99:31 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 97:16-99:31 {a:'Nat} -> 'VecS V1 a -> 'Bool testdata/Builtins.lc 97:16-99:31 'VecS V1 V0 -> 'Bool testdata/Builtins.lc 97:16-99:31 'Bool testdata/Builtins.lc 97:23-97:27 V1 -> V2->V2 testdata/Builtins.lc 97:23-97:27 V2->V2 testdata/Builtins.lc 97:23-97:27 V2 testdata/Builtins.lc 97:23-97:27 'Bool testdata/Builtins.lc 98:25-98:29 V0 -> V1 -> V2->'Bool testdata/Builtins.lc 98:25-98:29 V1 -> V2->'Bool testdata/Builtins.lc 98:25-98:29 V2->'Bool testdata/Builtins.lc 98:25-98:29 'Bool testdata/Builtins.lc 99:27-99:31 V0 -> V1 -> V2 -> V3->'Bool testdata/Builtins.lc 99:27-99:31 V1 -> V2 -> V3->'Bool testdata/Builtins.lc 99:27-99:31 V2 -> V3->'Bool testdata/Builtins.lc 99:27-99:31 V3->'Bool testdata/Builtins.lc 99:27-99:31 'Bool testdata/Builtins.lc 97:16-97:19 'VecS V1 V0 testdata/Builtins.lc 97:16-97:19 'VecS V4 V3 testdata/Builtins.lc 97:1-97:11 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 101:38-101:71 Type testdata/Builtins.lc 101:38-101:41 'Nat -> Type->Type testdata/Builtins.lc 101:42-101:43 'Nat testdata/Builtins.lc 101:42-101:43 V3 testdata/Builtins.lc 101:38-101:71 V4 testdata/Builtins.lc 101:49-101:52 'Nat -> Type->Type testdata/Builtins.lc 101:53-101:54 'Nat testdata/Builtins.lc 101:53-101:54 V2 testdata/Builtins.lc 101:55-101:60 Type testdata/Builtins.lc 101:64-101:67 'Nat -> Type->Type testdata/Builtins.lc 101:68-101:69 'Nat testdata/Builtins.lc 102:19-102:53 {a} -> {b:'Nat} -> {c:'Nat} -> 'VecS a b -> 'VecS 'Swizz c -> 'VecS a c testdata/Builtins.lc 102:19-102:53 {a:'Nat} -> {b:'Nat} -> 'VecS V2 a -> 'VecS 'Swizz b -> 'VecS V4 b testdata/Builtins.lc 102:19-102:53 {a:'Nat} -> 'VecS V2 V1 -> 'VecS 'Swizz a -> 'VecS V4 a testdata/Builtins.lc 102:19-102:53 'VecS V2 V1 -> 'VecS 'Swizz V1 -> 'VecS V4 V2 testdata/Builtins.lc 102:19-102:53 'VecS 'Swizz V1 -> 'VecS V4 V2 testdata/Builtins.lc 102:19-102:53 'VecS V4 V2 testdata/Builtins.lc 102:34-102:53 V0 testdata/Builtins.lc 102:34-102:40 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 102:42-102:53 V2->V2 testdata/Builtins.lc 102:42-102:53 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 102:19-102:31 'Bool testdata/Builtins.lc 102:19-102:29 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 102:30-102:31 'VecS V1 V0 testdata/Builtins.lc 102:30-102:31 'VecS V6 V5 testdata/Builtins.lc 102:1-102:12 {a} -> {b:'Nat} -> {c:'Nat} -> 'VecS a b -> 'VecS 'Swizz c -> 'VecS a c testdata/Builtins.lc 109:10-110:30 V0->Type testdata/Builtins.lc 109:10-110:30 Type testdata/Builtins.lc 109:10-109:16 Type testdata/Builtins.lc 109:25-109:28 Type testdata/Builtins.lc 109:25-109:28 V1 testdata/Builtins.lc 110:10-110:30 Type testdata/Builtins.lc 110:10-110:16 Type testdata/Builtins.lc 110:25-110:30 Type testdata/Builtins.lc 107:7-107:13 Type->Type testdata/Builtins.lc 117:10-125:19 V0->Type testdata/Builtins.lc 117:10-125:19 Type testdata/Builtins.lc 117:10-117:13 Type testdata/Builtins.lc 117:14-117:17 Type testdata/Builtins.lc 117:14-117:17 V1 testdata/Builtins.lc 121:10-125:19 Type testdata/Builtins.lc 121:10-121:13 Type testdata/Builtins.lc 121:14-121:18 Type testdata/Builtins.lc 125:10-125:19 Type testdata/Builtins.lc 125:10-125:13 Type testdata/Builtins.lc 125:14-125:19 Type testdata/Builtins.lc 112:7-112:10 Type->Type testdata/Builtins.lc 112:7-113:22 Type testdata/Builtins.lc 113:14-113:22 Type testdata/Builtins.lc 113:14-113:17 Type testdata/Builtins.lc 113:21-113:22 Type testdata/Builtins.lc 117:14-126:27 {a} -> {b : 'Num a} -> 'Int->a testdata/Builtins.lc 117:14-126:27 {a : 'Num V0} -> 'Int->V2 testdata/Builtins.lc 118:13-118:15 {a:'Unit} -> 'Int->'Int testdata/Builtins.lc 118:13-118:15 'Int->'Int testdata/Builtins.lc 118:13-118:15 {a} -> a->a testdata/Builtins.lc 121:14-126:27 {a : 'Num V0} -> 'Int->V2 testdata/Builtins.lc 122:13-122:26 {a:'Unit} -> 'Int->'Word testdata/Builtins.lc 122:13-122:26 'Int->'Word testdata/Builtins.lc 125:14-126:27 {a : 'Num V0} -> 'Int->V2 testdata/Builtins.lc 126:13-126:27 {a:'Unit} -> 'Int->'Float testdata/Builtins.lc 126:13-126:27 'Int->'Float testdata/Builtins.lc 113:3-113:10 {a} -> {b : 'Num a} -> 'Int->a testdata/Builtins.lc 112:7-114:32 Type testdata/Builtins.lc 114:14-114:32 Type testdata/Builtins.lc 114:14-114:15 Type testdata/Builtins.lc 114:19-114:32 Type testdata/Builtins.lc 114:19-114:20 Type testdata/Builtins.lc 114:24-114:32 Type testdata/Builtins.lc 117:14-127:29 {a} -> {b : 'Num a} -> a -> a->'Ordering testdata/Builtins.lc 117:14-127:29 {a : 'Num V0} -> V1 -> V2->'Ordering testdata/Builtins.lc 119:13-119:27 {a:'Unit} -> 'Int -> 'Int->'Ordering testdata/Builtins.lc 119:13-119:27 'Int -> 'Int->'Ordering testdata/Builtins.lc 121:14-127:29 {a : 'Num V0} -> V1 -> V2->'Ordering testdata/Builtins.lc 123:13-123:28 {a:'Unit} -> 'Word -> 'Word->'Ordering testdata/Builtins.lc 123:13-123:28 'Word -> 'Word->'Ordering testdata/Builtins.lc 125:14-127:29 {a : 'Num V0} -> V1 -> V2->'Ordering testdata/Builtins.lc 127:13-127:29 {a:'Unit} -> 'Float -> 'Float->'Ordering testdata/Builtins.lc 127:13-127:29 'Float -> 'Float->'Ordering testdata/Builtins.lc 114:3-114:10 {a} -> {b : 'Num a} -> a -> a->'Ordering testdata/Builtins.lc 112:7-115:19 Type testdata/Builtins.lc 115:13-115:19 Type testdata/Builtins.lc 115:13-115:14 Type testdata/Builtins.lc 115:18-115:19 Type testdata/Builtins.lc 117:14-128:27 {a} -> {b : 'Num a} -> a->a testdata/Builtins.lc 117:14-128:27 {a : 'Num V0} -> V1->V2 testdata/Builtins.lc 120:12-120:25 {a:'Unit} -> 'Int->'Int testdata/Builtins.lc 120:12-120:25 'Int->'Int testdata/Builtins.lc 121:14-128:27 {a : 'Num V0} -> V1->V2 testdata/Builtins.lc 124:12-124:26 {a:'Unit} -> 'Word->'Word testdata/Builtins.lc 124:12-124:26 'Word->'Word testdata/Builtins.lc 125:14-128:27 {a : 'Num V0} -> V1->V2 testdata/Builtins.lc 128:12-128:27 {a:'Unit} -> 'Float->'Float testdata/Builtins.lc 128:12-128:27 'Float->'Float testdata/Builtins.lc 115:3-115:9 {a} -> {b : 'Num a} -> a->a testdata/Builtins.lc 138:10-184:19 V0->Type testdata/Builtins.lc 138:10-184:19 Type testdata/Builtins.lc 138:10-138:19 Type testdata/Builtins.lc 138:20-138:24 Type testdata/Builtins.lc 138:20-138:24 V1 testdata/Builtins.lc 144:10-184:19 Type testdata/Builtins.lc 144:10-144:19 Type testdata/Builtins.lc 144:20-144:23 Type testdata/Builtins.lc 151:10-184:19 Type testdata/Builtins.lc 151:10-151:19 Type testdata/Builtins.lc 151:20-151:24 Type testdata/Builtins.lc 158:10-184:19 Type testdata/Builtins.lc 158:10-158:19 Type testdata/Builtins.lc 158:20-158:25 Type testdata/Builtins.lc 164:10-184:19 Type testdata/Builtins.lc 164:10-184:19 Type -> 'Nat->Type testdata/Builtins.lc 164:10-184:19 'Nat->Type testdata/Builtins.lc 164:10-176:19 Type testdata/Builtins.lc 164:10-176:19 'Nat->Type testdata/Builtins.lc 164:10-164:19 Type testdata/Builtins.lc 170:10-176:19 'Nat->Type testdata/Builtins.lc 170:10-176:19 Type testdata/Builtins.lc 170:10-170:19 Type testdata/Builtins.lc 176:10-176:19 'Nat->Type testdata/Builtins.lc 176:10-176:19 Type testdata/Builtins.lc 182:10-184:19 Type testdata/Builtins.lc 182:10-184:19 'Nat->Type testdata/Builtins.lc 182:10-182:19 Type testdata/Builtins.lc 183:10-184:19 'Nat->Type testdata/Builtins.lc 183:10-184:19 Type testdata/Builtins.lc 183:10-183:19 Type testdata/Builtins.lc 184:10-184:19 'Nat->Type testdata/Builtins.lc 184:10-184:19 Type testdata/Builtins.lc 164:26-164:33 Type testdata/Builtins.lc 130:7-130:16 Type->Type testdata/Builtins.lc 130:7-131:28 Type testdata/Builtins.lc 131:11-131:28 Type testdata/Builtins.lc 131:11-131:12 Type testdata/Builtins.lc 131:16-131:28 Type testdata/Builtins.lc 131:16-131:17 Type testdata/Builtins.lc 131:21-131:28 Type testdata/Builtins.lc 131:21-131:24 'Nat -> Type->Type testdata/Builtins.lc 131:27-131:28 Type testdata/Builtins.lc 138:20-185:12 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 138:20-185:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 139:10-139:12 {a:'Unit} -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 139:10-139:12 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 139:10-139:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 144:20-185:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 145:10-145:12 {a:'Unit} -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 145:10-145:12 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 145:10-145:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 151:20-185:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 152:10-152:12 {a:'Unit} -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 152:10-152:12 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 152:10-152:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 158:20-185:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 159:10-159:12 {a:'Unit} -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 159:10-159:12 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 159:10-159:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 164:26-185:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 165:10-185:12 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b -> 'VecS a b -> 'VecS ('VecS a b) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-185:12 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a -> 'VecS V3 a -> 'VecS ('VecS V4 a) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-185:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-177:12 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 -> 'VecS 'Float V2 -> 'VecS ('VecS 'Float V3) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-177:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS ('VecS 'Float (Succ a)) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-177:12 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) -> 'VecS 'Float (Succ V2) -> 'VecS ('VecS 'Float (Succ V3)) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-177:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS ('VecS 'Float (Succ (Succ a))) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-177:12 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) -> 'VecS 'Float (Succ (Succ V2)) -> 'VecS ('VecS 'Float (Succ (Succ V3))) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-165:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-165:12 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ Zero)) testdata/Builtins.lc 165:10-165:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 171:10-177:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ a)))) (Succ (Succ Zero)) testdata/Builtins.lc 171:10-177:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) -> 'VecS 'Float (Succ (Succ (Succ V2))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ V3)))) (Succ (Succ Zero)) testdata/Builtins.lc 171:10-171:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ Zero)) testdata/Builtins.lc 171:10-171:12 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ Zero)) testdata/Builtins.lc 171:10-171:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 177:10-177:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ a))))) (Succ (Succ Zero)) testdata/Builtins.lc 177:10-177:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V2)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ V3))))) (Succ (Succ Zero)) testdata/Builtins.lc 177:10-177:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ Zero)) testdata/Builtins.lc 177:10-177:12 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ Zero)) testdata/Builtins.lc 177:10-177:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 -> 'VecS 'Bool V2 -> 'VecS ('VecS 'Bool V3) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS ('VecS 'Bool (Succ a)) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) -> 'VecS 'Bool (Succ V2) -> 'VecS ('VecS 'Bool (Succ V3)) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS ('VecS 'Bool (Succ (Succ a))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) -> 'VecS 'Bool (Succ (Succ V2)) -> 'VecS ('VecS 'Bool (Succ (Succ V3))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ a)))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) -> 'VecS 'Bool (Succ (Succ (Succ V2))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ V3)))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ a))))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V2)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ V3))))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ Zero)) testdata/Builtins.lc 185:10-185:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 131:3-131:7 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 130:7-132:33 Type testdata/Builtins.lc 132:11-132:33 Type testdata/Builtins.lc 132:11-132:12 Type testdata/Builtins.lc 132:16-132:33 Type testdata/Builtins.lc 132:16-132:17 Type testdata/Builtins.lc 132:21-132:33 Type testdata/Builtins.lc 132:21-132:22 Type testdata/Builtins.lc 132:26-132:33 Type testdata/Builtins.lc 132:26-132:29 'Nat -> Type->Type testdata/Builtins.lc 132:32-132:33 Type testdata/Builtins.lc 138:20-186:12 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 138:20-186:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 140:10-140:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 140:10-140:12 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 140:10-140:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 144:20-186:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 146:10-146:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 146:10-146:12 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 146:10-146:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 151:20-186:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 153:10-153:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 153:10-153:12 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 153:10-153:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 158:20-186:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 160:10-160:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 160:10-160:12 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 160:10-160:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 164:26-186:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-186:12 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b -> 'VecS a b -> 'VecS a b -> 'VecS ('VecS a b) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-186:12 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a -> 'VecS V3 a -> 'VecS V4 a -> 'VecS ('VecS V5 a) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-186:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS V4 V3 -> 'VecS ('VecS V5 V4) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-178:12 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 -> 'VecS 'Float V2 -> 'VecS 'Float V3 -> 'VecS ('VecS 'Float V4) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-178:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS ('VecS 'Float (Succ a)) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-178:12 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) -> 'VecS 'Float (Succ V2) -> 'VecS 'Float (Succ V3) -> 'VecS ('VecS 'Float (Succ V4)) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-178:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS ('VecS 'Float (Succ (Succ a))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-178:12 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) -> 'VecS 'Float (Succ (Succ V2)) -> 'VecS 'Float (Succ (Succ V3)) -> 'VecS ('VecS 'Float (Succ (Succ V4))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-166:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-166:12 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 166:10-166:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 172:10-178:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ a)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 172:10-178:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) -> 'VecS 'Float (Succ (Succ (Succ V2))) -> 'VecS 'Float (Succ (Succ (Succ V3))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ V4)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 172:10-172:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 172:10-172:12 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 172:10-172:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 178:10-178:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ a))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 178:10-178:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V2)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V3)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ V4))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 178:10-178:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 178:10-178:12 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 178:10-178:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS V4 V3 -> 'VecS ('VecS V5 V4) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 -> 'VecS 'Bool V2 -> 'VecS 'Bool V3 -> 'VecS ('VecS 'Bool V4) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS ('VecS 'Bool (Succ a)) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) -> 'VecS 'Bool (Succ V2) -> 'VecS 'Bool (Succ V3) -> 'VecS ('VecS 'Bool (Succ V4)) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS ('VecS 'Bool (Succ (Succ a))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) -> 'VecS 'Bool (Succ (Succ V2)) -> 'VecS 'Bool (Succ (Succ V3)) -> 'VecS ('VecS 'Bool (Succ (Succ V4))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ a)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) -> 'VecS 'Bool (Succ (Succ (Succ V2))) -> 'VecS 'Bool (Succ (Succ (Succ V3))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ V4)))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ a))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V2)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V3)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ V4))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ Zero))) testdata/Builtins.lc 186:10-186:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 132:3-132:7 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 130:7-133:38 Type testdata/Builtins.lc 133:11-133:38 Type testdata/Builtins.lc 133:11-133:12 Type testdata/Builtins.lc 133:16-133:38 Type testdata/Builtins.lc 133:16-133:17 Type testdata/Builtins.lc 133:21-133:38 Type testdata/Builtins.lc 133:21-133:22 Type testdata/Builtins.lc 133:26-133:38 Type testdata/Builtins.lc 133:26-133:27 Type testdata/Builtins.lc 133:31-133:38 Type testdata/Builtins.lc 133:31-133:34 'Nat -> Type->Type testdata/Builtins.lc 133:37-133:38 Type testdata/Builtins.lc 138:20-187:12 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 138:20-187:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 141:10-141:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 141:10-141:12 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 141:10-141:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 144:20-187:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 147:10-147:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 147:10-147:12 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 147:10-147:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 151:20-187:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 154:10-154:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 154:10-154:12 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 154:10-154:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 158:20-187:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 161:10-161:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 161:10-161:12 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 161:10-161:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 164:26-187:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-187:12 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b -> 'VecS a b -> 'VecS a b -> 'VecS a b -> 'VecS ('VecS a b) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-187:12 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a -> 'VecS V3 a -> 'VecS V4 a -> 'VecS V5 a -> 'VecS ('VecS V6 a) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-187:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS V4 V3 -> 'VecS V5 V4 -> 'VecS ('VecS V6 V5) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-179:12 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 -> 'VecS 'Float V2 -> 'VecS 'Float V3 -> 'VecS 'Float V4 -> 'VecS ('VecS 'Float V5) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-179:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS 'Float (Succ a) -> 'VecS ('VecS 'Float (Succ a)) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-179:12 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) -> 'VecS 'Float (Succ V2) -> 'VecS 'Float (Succ V3) -> 'VecS 'Float (Succ V4) -> 'VecS ('VecS 'Float (Succ V5)) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-179:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS 'Float (Succ (Succ a)) -> 'VecS ('VecS 'Float (Succ (Succ a))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-179:12 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) -> 'VecS 'Float (Succ (Succ V2)) -> 'VecS 'Float (Succ (Succ V3)) -> 'VecS 'Float (Succ (Succ V4)) -> 'VecS ('VecS 'Float (Succ (Succ V5))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-167:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-167:12 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:10-167:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 173:10-179:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS 'Float (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ a)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 173:10-179:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) -> 'VecS 'Float (Succ (Succ (Succ V2))) -> 'VecS 'Float (Succ (Succ (Succ V3))) -> 'VecS 'Float (Succ (Succ (Succ V4))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ V5)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 173:10-173:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 173:10-173:12 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 173:10-173:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 179:10-179:12 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ a))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 179:10-179:12 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V2)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V3)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ V4)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ V5))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 179:10-179:12 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 179:10-179:12 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 179:10-179:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS V4 V3 -> 'VecS V5 V4 -> 'VecS ('VecS V6 V5) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 -> 'VecS 'Bool V2 -> 'VecS 'Bool V3 -> 'VecS 'Bool V4 -> 'VecS ('VecS 'Bool V5) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS 'Bool (Succ a) -> 'VecS ('VecS 'Bool (Succ a)) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) -> 'VecS 'Bool (Succ V2) -> 'VecS 'Bool (Succ V3) -> 'VecS 'Bool (Succ V4) -> 'VecS ('VecS 'Bool (Succ V5)) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS 'Bool (Succ (Succ a)) -> 'VecS ('VecS 'Bool (Succ (Succ a))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) -> 'VecS 'Bool (Succ (Succ V2)) -> 'VecS 'Bool (Succ (Succ V3)) -> 'VecS 'Bool (Succ (Succ V4)) -> 'VecS ('VecS 'Bool (Succ (Succ V5))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS 'Bool (Succ (Succ (Succ a))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ a)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) -> 'VecS 'Bool (Succ (Succ (Succ V2))) -> 'VecS 'Bool (Succ (Succ (Succ V3))) -> 'VecS 'Bool (Succ (Succ (Succ V4))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ V5)))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ a))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V2)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V3)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ V4)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ V5))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) -> 'VecS ('VecS 'Bool (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 187:10-187:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 133:3-133:7 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 130:7-134:16 Type testdata/Builtins.lc 134:15-134:16 Type testdata/Builtins.lc 138:20-188:40 {a} -> {b : 'Component a}->a testdata/Builtins.lc 138:20-188:40 {a : 'Component V0}->V1 testdata/Builtins.lc 142:14-142:19 {a:'Unit}->'Bool testdata/Builtins.lc 142:14-142:19 'Bool testdata/Builtins.lc 144:20-188:40 {a : 'Component V0}->V1 testdata/Builtins.lc 148:14-148:22 {a:'Unit}->'Int testdata/Builtins.lc 148:19-148:22 Type testdata/Builtins.lc 148:14-148:15 'Int testdata/Builtins.lc 151:20-188:40 {a : 'Component V0}->V1 testdata/Builtins.lc 155:14-155:23 {a:'Unit}->'Word testdata/Builtins.lc 155:19-155:23 Type testdata/Builtins.lc 155:14-155:15 'Word testdata/Builtins.lc 155:14-155:15 'Int testdata/Builtins.lc 158:20-188:40 {a : 'Component V0}->V1 testdata/Builtins.lc 162:14-162:17 {a:'Unit}->'Float testdata/Builtins.lc 162:14-162:17 'Float testdata/Builtins.lc 164:26-188:40 {a : 'Component V0}->V1 testdata/Builtins.lc 168:14-188:40 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 168:14-188:40 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 168:14-188:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 168:14-180:32 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 168:14-180:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 168:14-180:32 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 168:14-180:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 168:14-180:32 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 168:14-168:24 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 168:14-168:16 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 168:17-168:20 V0 testdata/Builtins.lc 168:17-168:20 'Float testdata/Builtins.lc 168:21-168:24 'Float testdata/Builtins.lc 174:14-180:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 174:14-180:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 174:14-174:28 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 174:14-174:16 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 174:17-174:20 V0 testdata/Builtins.lc 174:17-174:20 'Float testdata/Builtins.lc 174:21-174:24 'Float testdata/Builtins.lc 174:25-174:28 'Float testdata/Builtins.lc 180:14-180:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 180:14-180:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 180:14-180:32 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 180:14-180:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 180:17-180:20 V0 testdata/Builtins.lc 180:17-180:20 'Float testdata/Builtins.lc 180:21-180:24 'Float testdata/Builtins.lc 180:25-180:28 'Float testdata/Builtins.lc 180:29-180:32 'Float testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 188:14-188:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 188:14-188:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 188:14-188:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 188:14-188:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 188:14-188:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 188:14-188:40 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 188:14-188:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 188:17-188:22 V0 testdata/Builtins.lc 188:17-188:22 'Bool testdata/Builtins.lc 188:23-188:28 'Bool testdata/Builtins.lc 188:29-188:34 'Bool testdata/Builtins.lc 188:35-188:40 'Bool testdata/Builtins.lc 134:3-134:11 {a} -> {b : 'Component a}->a testdata/Builtins.lc 130:7-135:15 Type testdata/Builtins.lc 135:14-135:15 Type testdata/Builtins.lc 138:20-189:35 {a} -> {b : 'Component a}->a testdata/Builtins.lc 138:20-189:35 {a : 'Component V0}->V1 testdata/Builtins.lc 143:13-143:17 {a:'Unit}->'Bool testdata/Builtins.lc 143:13-143:17 'Bool testdata/Builtins.lc 144:20-189:35 {a : 'Component V0}->V1 testdata/Builtins.lc 149:13-149:21 {a:'Unit}->'Int testdata/Builtins.lc 149:18-149:21 Type testdata/Builtins.lc 149:13-149:14 'Int testdata/Builtins.lc 151:20-189:35 {a : 'Component V0}->V1 testdata/Builtins.lc 156:13-156:22 {a:'Unit}->'Word testdata/Builtins.lc 156:18-156:22 Type testdata/Builtins.lc 156:13-156:14 'Word testdata/Builtins.lc 156:13-156:14 'Int testdata/Builtins.lc 158:20-189:35 {a : 'Component V0}->V1 testdata/Builtins.lc 163:13-163:16 {a:'Unit}->'Float testdata/Builtins.lc 163:13-163:16 'Float testdata/Builtins.lc 164:26-189:35 {a : 'Component V0}->V1 testdata/Builtins.lc 169:13-189:35 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 169:13-189:35 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 169:13-189:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 169:13-181:31 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 169:13-181:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 169:13-181:31 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 169:13-181:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 169:13-181:31 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 169:13-169:23 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 169:13-169:15 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 169:16-169:19 V0 testdata/Builtins.lc 169:16-169:19 'Float testdata/Builtins.lc 169:20-169:23 'Float testdata/Builtins.lc 175:13-181:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 175:13-181:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 175:13-175:27 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 175:13-175:15 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 175:16-175:19 V0 testdata/Builtins.lc 175:16-175:19 'Float testdata/Builtins.lc 175:20-175:23 'Float testdata/Builtins.lc 175:24-175:27 'Float testdata/Builtins.lc 181:13-181:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 181:13-181:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 181:13-181:31 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 181:13-181:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 181:16-181:19 V0 testdata/Builtins.lc 181:16-181:19 'Float testdata/Builtins.lc 181:20-181:23 'Float testdata/Builtins.lc 181:24-181:27 'Float testdata/Builtins.lc 181:28-181:31 'Float testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 189:13-189:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 189:13-189:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 189:13-189:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 189:13-189:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 189:13-189:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 189:13-189:35 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 189:13-189:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 189:16-189:20 V0 testdata/Builtins.lc 189:16-189:20 'Bool testdata/Builtins.lc 189:21-189:25 'Bool testdata/Builtins.lc 189:26-189:30 'Bool testdata/Builtins.lc 189:31-189:35 'Bool testdata/Builtins.lc 135:3-135:10 {a} -> {b : 'Component a}->a testdata/Builtins.lc 193:10-194:29 V0->Type testdata/Builtins.lc 193:10-194:29 Type testdata/Builtins.lc 193:10-193:18 Type testdata/Builtins.lc 193:25-193:28 Type testdata/Builtins.lc 193:25-193:28 V1 testdata/Builtins.lc 194:10-194:29 Type testdata/Builtins.lc 194:10-194:18 Type testdata/Builtins.lc 194:25-194:29 Type testdata/Builtins.lc 191:7-191:15 Type->Type testdata/Builtins.lc 198:10-210:18 V0->Type testdata/Builtins.lc 198:10-210:18 Type testdata/Builtins.lc 198:10-198:18 Type testdata/Builtins.lc 198:25-198:30 Type testdata/Builtins.lc 198:25-198:30 V1 testdata/Builtins.lc 199:10-210:18 Type testdata/Builtins.lc 199:10-201:18 Type -> 'Nat->Type testdata/Builtins.lc 199:10-201:18 'Nat->Type testdata/Builtins.lc 199:10-201:18 Type testdata/Builtins.lc 199:10-199:18 Type testdata/Builtins.lc 200:10-201:18 'Nat->Type testdata/Builtins.lc 200:10-201:18 Type testdata/Builtins.lc 200:10-200:18 Type testdata/Builtins.lc 201:10-201:18 'Nat->Type testdata/Builtins.lc 201:10-201:18 Type testdata/Builtins.lc 199:31-199:38 Type testdata/Builtins.lc 202:10-210:18 Type testdata/Builtins.lc 202:10-210:18 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 202:10-210:18 'Nat -> Type->Type testdata/Builtins.lc 202:10-210:18 Type->Type testdata/Builtins.lc 202:10-210:18 'Nat->Type testdata/Builtins.lc 202:10-204:18 Type testdata/Builtins.lc 202:10-204:18 'Nat->Type testdata/Builtins.lc 202:10-202:18 Type testdata/Builtins.lc 203:10-204:18 'Nat->Type testdata/Builtins.lc 203:10-204:18 Type testdata/Builtins.lc 203:10-203:18 Type testdata/Builtins.lc 204:10-204:18 'Nat->Type testdata/Builtins.lc 204:10-204:18 Type testdata/Builtins.lc 205:10-210:18 'Nat->Type testdata/Builtins.lc 205:10-210:18 Type testdata/Builtins.lc 205:10-207:18 Type testdata/Builtins.lc 205:10-207:18 'Nat->Type testdata/Builtins.lc 205:10-205:18 Type testdata/Builtins.lc 206:10-207:18 'Nat->Type testdata/Builtins.lc 206:10-207:18 Type testdata/Builtins.lc 206:10-206:18 Type testdata/Builtins.lc 207:10-207:18 'Nat->Type testdata/Builtins.lc 207:10-207:18 Type testdata/Builtins.lc 208:10-210:18 'Nat->Type testdata/Builtins.lc 208:10-210:18 Type testdata/Builtins.lc 208:10-208:18 Type testdata/Builtins.lc 209:10-210:18 'Nat->Type testdata/Builtins.lc 209:10-210:18 Type testdata/Builtins.lc 209:10-209:18 Type testdata/Builtins.lc 210:10-210:18 'Nat->Type testdata/Builtins.lc 210:10-210:18 Type testdata/Builtins.lc 202:30-202:39 Type testdata/Builtins.lc 196:7-196:15 Type->Type testdata/Builtins.lc 212:6-212:20 Type testdata/Builtins.lc 213:7-213:12 'BlendingFactor testdata/Builtins.lc 214:7-214:10 'BlendingFactor testdata/Builtins.lc 215:7-215:15 'BlendingFactor testdata/Builtins.lc 216:7-216:23 'BlendingFactor testdata/Builtins.lc 217:7-217:15 'BlendingFactor testdata/Builtins.lc 218:7-218:23 'BlendingFactor testdata/Builtins.lc 219:7-219:15 'BlendingFactor testdata/Builtins.lc 220:7-220:23 'BlendingFactor testdata/Builtins.lc 221:7-221:15 'BlendingFactor testdata/Builtins.lc 222:7-222:23 'BlendingFactor testdata/Builtins.lc 223:7-223:20 'BlendingFactor testdata/Builtins.lc 224:7-224:28 'BlendingFactor testdata/Builtins.lc 225:7-225:20 'BlendingFactor testdata/Builtins.lc 226:7-226:28 'BlendingFactor testdata/Builtins.lc 227:7-227:23 'BlendingFactor testdata/Builtins.lc 229:6-229:19 Type testdata/Builtins.lc 230:7-230:14 'BlendEquation testdata/Builtins.lc 231:7-231:19 'BlendEquation testdata/Builtins.lc 232:7-232:26 'BlendEquation testdata/Builtins.lc 233:7-233:10 'BlendEquation testdata/Builtins.lc 234:7-234:10 'BlendEquation testdata/Builtins.lc 236:6-236:20 Type testdata/Builtins.lc 237:7-237:12 'LogicOperation testdata/Builtins.lc 238:7-238:10 'LogicOperation testdata/Builtins.lc 239:7-239:17 'LogicOperation testdata/Builtins.lc 240:7-240:11 'LogicOperation testdata/Builtins.lc 241:7-241:18 'LogicOperation testdata/Builtins.lc 242:7-242:11 'LogicOperation testdata/Builtins.lc 243:7-243:10 'LogicOperation testdata/Builtins.lc 244:7-244:9 'LogicOperation testdata/Builtins.lc 245:7-245:10 'LogicOperation testdata/Builtins.lc 246:7-246:12 'LogicOperation testdata/Builtins.lc 247:7-247:13 'LogicOperation testdata/Builtins.lc 248:7-248:16 'LogicOperation testdata/Builtins.lc 249:7-249:19 'LogicOperation testdata/Builtins.lc 250:7-250:17 'LogicOperation testdata/Builtins.lc 251:7-251:11 'LogicOperation testdata/Builtins.lc 252:7-252:10 'LogicOperation testdata/Builtins.lc 254:6-254:22 Type testdata/Builtins.lc 255:7-255:13 'StencilOperation testdata/Builtins.lc 256:7-256:13 'StencilOperation testdata/Builtins.lc 257:7-257:16 'StencilOperation testdata/Builtins.lc 258:7-258:13 'StencilOperation testdata/Builtins.lc 259:7-259:17 'StencilOperation testdata/Builtins.lc 260:7-260:13 'StencilOperation testdata/Builtins.lc 261:7-261:17 'StencilOperation testdata/Builtins.lc 262:7-262:15 'StencilOperation testdata/Builtins.lc 264:6-264:24 Type testdata/Builtins.lc 265:7-265:12 'ComparisonFunction testdata/Builtins.lc 266:7-266:11 'ComparisonFunction testdata/Builtins.lc 267:7-267:12 'ComparisonFunction testdata/Builtins.lc 268:7-268:13 'ComparisonFunction testdata/Builtins.lc 269:7-269:14 'ComparisonFunction testdata/Builtins.lc 270:7-270:15 'ComparisonFunction testdata/Builtins.lc 271:7-271:13 'ComparisonFunction testdata/Builtins.lc 272:7-272:13 'ComparisonFunction testdata/Builtins.lc 274:6-274:21 Type testdata/Builtins.lc 275:7-275:17 'ProvokingVertex testdata/Builtins.lc 276:7-276:18 'ProvokingVertex testdata/Builtins.lc 278:6-278:14 Type testdata/Builtins.lc 279:7-279:16 'CullMode testdata/Builtins.lc 280:7-280:15 'CullMode testdata/Builtins.lc 281:7-281:15 'CullMode testdata/Builtins.lc 283:6-283:15 Type testdata/Builtins.lc 284:17-284:22 Type testdata/Builtins.lc 284:7-284:16 'Float->'PointSize testdata/Builtins.lc 285:7-285:23 'PointSize testdata/Builtins.lc 287:6-287:17 Type testdata/Builtins.lc 288:7-288:18 'PolygonMode testdata/Builtins.lc 289:20-289:29 Type testdata/Builtins.lc 289:7-289:19 'PointSize->'PolygonMode testdata/Builtins.lc 290:19-290:24 Type testdata/Builtins.lc 290:7-290:18 'Float->'PolygonMode testdata/Builtins.lc 292:6-292:19 Type testdata/Builtins.lc 293:7-293:15 'PolygonOffset testdata/Builtins.lc 294:14-294:19 Type testdata/Builtins.lc 292:6-294:25 Type testdata/Builtins.lc 294:20-294:25 Type testdata/Builtins.lc 294:7-294:13 'Float -> 'Float->'PolygonOffset testdata/Builtins.lc 296:6-296:28 Type testdata/Builtins.lc 297:7-297:16 'PointSpriteCoordOrigin testdata/Builtins.lc 298:7-298:16 'PointSpriteCoordOrigin testdata/Builtins.lc 301:6-301:11 Type->Type testdata/Builtins.lc 302:6-302:13 Type->Type testdata/Builtins.lc 303:6-303:11 Type->Type testdata/Builtins.lc 305:6-305:19 Type testdata/Builtins.lc 306:7-306:15 'PrimitiveType testdata/Builtins.lc 307:7-307:11 'PrimitiveType testdata/Builtins.lc 308:7-308:12 'PrimitiveType testdata/Builtins.lc 309:7-309:24 'PrimitiveType testdata/Builtins.lc 310:7-310:20 'PrimitiveType testdata/Builtins.lc 313:16-313:18 Type testdata/Builtins.lc 313:22-313:48 Type testdata/Builtins.lc 313:22-313:25 'Nat -> Type->Type testdata/Builtins.lc 313:28-313:33 Type testdata/Builtins.lc 313:37-313:48 Type testdata/Builtins.lc 313:37-313:40 'Nat -> Type->Type testdata/Builtins.lc 313:43-313:48 Type testdata/Builtins.lc 313:1-313:12 'Tuple0 -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 316:14-316:25 Type testdata/Builtins.lc 316:14-316:20 Type testdata/Builtins.lc 316:14-316:25 V2 testdata/Builtins.lc 316:1-316:8 {a} -> 'String->a testdata/Builtins.lc 317:14-317:25 Type testdata/Builtins.lc 317:14-317:20 Type testdata/Builtins.lc 317:14-317:25 V2 testdata/Builtins.lc 317:1-317:10 {a} -> 'String->a testdata/Builtins.lc 319:23-319:36 Type testdata/Builtins.lc 319:40-319:44 Type testdata/Builtins.lc 319:6-319:19 'PrimitiveType->Type testdata/Builtins.lc 320:26-320:34 Type testdata/Builtins.lc 320:38-320:111 Type testdata/Builtins.lc 320:38-320:49 Type testdata/Builtins.lc 320:53-320:111 Type testdata/Builtins.lc 320:53-320:66 Type testdata/Builtins.lc 320:70-320:111 Type testdata/Builtins.lc 320:70-320:85 Type testdata/Builtins.lc 320:89-320:111 Type testdata/Builtins.lc 320:89-320:102 'PrimitiveType->Type testdata/Builtins.lc 320:103-320:111 'PrimitiveType testdata/Builtins.lc 320:3-320:14 'CullMode -> 'PolygonMode -> 'PolygonOffset -> 'ProvokingVertex -> 'RasterContext Triangle testdata/Builtins.lc 321:26-321:35 Type testdata/Builtins.lc 321:39-321:108 Type testdata/Builtins.lc 321:39-321:44 Type testdata/Builtins.lc 321:48-321:108 Type testdata/Builtins.lc 321:48-321:70 Type testdata/Builtins.lc 321:89-321:108 Type testdata/Builtins.lc 321:89-321:102 'PrimitiveType->Type testdata/Builtins.lc 321:103-321:108 'PrimitiveType testdata/Builtins.lc 321:3-321:11 'PointSize -> 'Float -> 'PointSpriteCoordOrigin -> 'RasterContext Point testdata/Builtins.lc 322:26-322:31 Type testdata/Builtins.lc 322:35-322:107 Type testdata/Builtins.lc 322:35-322:50 Type testdata/Builtins.lc 322:89-322:107 Type testdata/Builtins.lc 322:89-322:102 'PrimitiveType->Type testdata/Builtins.lc 322:103-322:107 'PrimitiveType testdata/Builtins.lc 322:3-322:10 'Float -> 'ProvokingVertex -> 'RasterContext Line testdata/Builtins.lc 320:103-322:107 Type testdata/Builtins.lc 320:103-320:111 Type testdata/Builtins.lc 321:103-322:107 Type testdata/Builtins.lc 321:103-321:108 Type testdata/Builtins.lc 322:103-322:107 Type testdata/Builtins.lc 324:6-324:18 Type->Type testdata/Builtins.lc 326:27-326:56 Type testdata/Builtins.lc 326:27-326:35 Type->Type testdata/Builtins.lc 326:36-326:37 Type testdata/Builtins.lc 326:42-326:56 Type testdata/Builtins.lc 326:42-326:54 Type->Type testdata/Builtins.lc 326:55-326:56 Type testdata/Builtins.lc 325:3-325:9 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 325:11-325:24 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 327:42-327:56 Type testdata/Builtins.lc 327:42-327:54 Type->Type testdata/Builtins.lc 327:55-327:56 Type testdata/Builtins.lc 327:3-327:7 {a} -> 'Interpolated a testdata/Builtins.lc 331:14-332:32 Type->Type testdata/Builtins.lc 331:14-332:32 Type testdata/Builtins.lc 331:14-331:15 Type testdata/Builtins.lc 332:15-332:32 Type testdata/Builtins.lc 332:26-332:32 Type -> Type->Type testdata/Builtins.lc 332:26-332:32 Type->Type testdata/Builtins.lc 332:26-332:32 Type testdata/Builtins.lc 332:15-332:21 Type testdata/Builtins.lc 331:5-331:12 Type->Type testdata/Builtins.lc 335:27-338:82 Type->Type testdata/Builtins.lc 335:27-338:82 Type testdata/Builtins.lc 335:27-335:29 Type testdata/Builtins.lc 336:36-338:82 Type testdata/Builtins.lc 336:36-336:37 Type testdata/Builtins.lc 337:23-338:82 Type testdata/Builtins.lc 337:57-337:63 Type -> Type->Type testdata/Builtins.lc 337:57-337:63 Type->Type testdata/Builtins.lc 337:57-337:63 Type testdata/Builtins.lc 337:23-337:53 Type testdata/Builtins.lc 338:23-338:82 Type testdata/Builtins.lc 338:73-338:82 Type -> Type -> Type->Type testdata/Builtins.lc 338:73-338:82 Type -> Type->Type testdata/Builtins.lc 338:73-338:82 Type->Type testdata/Builtins.lc 338:73-338:82 Type testdata/Builtins.lc 338:23-338:69 Type testdata/Builtins.lc 335:5-335:21 Type->Type testdata/Builtins.lc 340:18-340:22 Type testdata/Builtins.lc 340:26-340:30 Type testdata/Builtins.lc 340:6-340:14 Type->Type testdata/Builtins.lc 341:60-341:70 Type testdata/Builtins.lc 341:60-341:68 Type->Type testdata/Builtins.lc 341:60-341:70 V1 testdata/Builtins.lc 341:3-341:13 {a} -> 'Blending a testdata/Builtins.lc 342:27-342:70 Type testdata/Builtins.lc 342:27-342:35 Type->Type testdata/Builtins.lc 342:27-342:70 V1 testdata/Builtins.lc 342:42-342:56 Type testdata/Builtins.lc 342:60-342:68 Type->Type testdata/Builtins.lc 342:3-342:15 {a} -> {b : 'Integral a} -> 'LogicOperation -> 'Blending a testdata/Builtins.lc 343:26-343:56 Type -> Type->Type testdata/Builtins.lc 343:27-343:40 Type testdata/Builtins.lc 343:42-343:55 Type testdata/Builtins.lc 344:29-345:74 Type testdata/Builtins.lc 344:29-344:97 Type -> Type->Type testdata/Builtins.lc 344:30-344:62 Type testdata/Builtins.lc 344:30-344:62 Type -> Type->Type testdata/Builtins.lc 344:31-344:45 Type testdata/Builtins.lc 344:47-344:61 Type testdata/Builtins.lc 344:64-344:96 Type testdata/Builtins.lc 344:64-344:96 Type -> Type->Type testdata/Builtins.lc 344:65-344:79 Type testdata/Builtins.lc 344:81-344:95 Type testdata/Builtins.lc 345:29-345:74 Type testdata/Builtins.lc 345:29-345:32 'Nat -> Type->Type testdata/Builtins.lc 345:35-345:40 Type testdata/Builtins.lc 345:60-345:74 Type testdata/Builtins.lc 345:60-345:68 Type->Type testdata/Builtins.lc 345:69-345:74 Type testdata/Builtins.lc 343:3-343:8 'Tuple2 'BlendEquation 'BlendEquation -> 'Tuple2 ('Tuple2 'BlendingFactor 'BlendingFactor) ('Tuple2 'BlendingFactor 'BlendingFactor) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Blending 'Float testdata/Builtins.lc 341:60-345:74 Type testdata/Builtins.lc 342:27-345:74 Type testdata/Builtins.lc 352:6-352:18 Type testdata/Builtins.lc 353:6-353:16 Type testdata/Builtins.lc 354:6-354:11 Type testdata/Builtins.lc 356:27-356:31 Type testdata/Builtins.lc 356:35-356:39 Type testdata/Builtins.lc 356:6-356:23 Type->Type testdata/Builtins.lc 357:27-358:101 Type testdata/Builtins.lc 357:27-358:101 V7 testdata/Builtins.lc 357:34-357:43 'Nat -> Type->Type testdata/Builtins.lc 357:27-358:101 'Nat testdata/Builtins.lc 357:27-358:101 V5 testdata/Builtins.lc 357:46-357:50 Type testdata/Builtins.lc 357:27-358:101 V4 testdata/Builtins.lc 357:60-357:69 'Nat -> Type->Type testdata/Builtins.lc 357:27-358:101 V2 testdata/Builtins.lc 357:75-357:78 Type->Type testdata/Builtins.lc 357:85-357:93 Type->Type testdata/Builtins.lc 358:71-358:88 Type->Type testdata/Builtins.lc 358:90-358:95 Type->Type testdata/Builtins.lc 357:3-357:10 {a} -> {b:'Nat} -> {c} -> {d} -> {e : a ~ 'VecScalar b 'Bool} -> {f : c ~ 'VecScalar b d} -> {g : 'Num d} -> 'Blending d -> a -> 'FragmentOperation ('Color c) testdata/Builtins.lc 359:26-359:44 Type testdata/Builtins.lc 359:48-359:101 Type testdata/Builtins.lc 359:48-359:52 Type testdata/Builtins.lc 359:71-359:101 Type testdata/Builtins.lc 359:71-359:88 Type->Type testdata/Builtins.lc 359:90-359:101 Type testdata/Builtins.lc 359:90-359:95 Type->Type testdata/Builtins.lc 359:96-359:101 Type testdata/Builtins.lc 359:3-359:10 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 360:26-360:38 Type testdata/Builtins.lc 360:42-360:103 Type testdata/Builtins.lc 360:42-360:52 Type testdata/Builtins.lc 360:56-360:103 Type testdata/Builtins.lc 360:56-360:66 Type testdata/Builtins.lc 360:71-360:103 Type testdata/Builtins.lc 360:71-360:88 Type->Type testdata/Builtins.lc 360:90-360:103 Type testdata/Builtins.lc 360:90-360:97 Type->Type testdata/Builtins.lc 360:98-360:103 Type testdata/Builtins.lc 360:3-360:12 'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation ('Stencil 'Int32) testdata/Builtins.lc 357:27-360:103 Type testdata/Builtins.lc 359:90-360:103 Type testdata/Builtins.lc 363:32-367:146 Type->Type testdata/Builtins.lc 363:32-367:146 Type testdata/Builtins.lc 363:32-363:33 Type testdata/Builtins.lc 364:14-367:146 Type testdata/Builtins.lc 364:60-364:68 Type -> Type->Type testdata/Builtins.lc 364:60-364:68 Type->Type testdata/Builtins.lc 364:60-364:68 Type testdata/Builtins.lc 364:14-364:56 Type testdata/Builtins.lc 365:14-367:146 Type testdata/Builtins.lc 365:82-365:94 Type -> Type -> Type->Type testdata/Builtins.lc 365:82-365:94 Type -> Type->Type testdata/Builtins.lc 365:82-365:94 Type->Type testdata/Builtins.lc 365:82-365:94 Type testdata/Builtins.lc 365:14-365:78 Type testdata/Builtins.lc 366:14-367:146 Type testdata/Builtins.lc 366:104-366:120 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 366:104-366:120 Type -> Type -> Type->Type testdata/Builtins.lc 366:104-366:120 Type -> Type->Type testdata/Builtins.lc 366:104-366:120 Type->Type testdata/Builtins.lc 366:104-366:120 Type testdata/Builtins.lc 366:14-366:100 Type testdata/Builtins.lc 367:14-367:146 Type testdata/Builtins.lc 367:126-367:146 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 367:126-367:146 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 367:126-367:146 Type -> Type -> Type->Type testdata/Builtins.lc 367:126-367:146 Type -> Type->Type testdata/Builtins.lc 367:126-367:146 Type->Type testdata/Builtins.lc 367:126-367:146 Type testdata/Builtins.lc 367:14-367:122 Type testdata/Builtins.lc 363:5-363:12 Type->Type testdata/Builtins.lc 370:15-374:36 Type->Type testdata/Builtins.lc 370:15-374:36 Type testdata/Builtins.lc 370:25-370:69 Type -> Type->Type testdata/Builtins.lc 370:25-370:69 Type->Type testdata/Builtins.lc 370:25-370:69 Type testdata/Builtins.lc 370:26-370:43 Type testdata/Builtins.lc 370:26-370:43 Type->Type testdata/Builtins.lc 370:48-370:65 Type testdata/Builtins.lc 370:48-370:65 Type->Type testdata/Builtins.lc 370:15-370:21 Type testdata/Builtins.lc 371:15-374:36 Type testdata/Builtins.lc 371:29-371:95 Type -> Type -> Type->Type testdata/Builtins.lc 371:29-371:95 Type -> Type->Type testdata/Builtins.lc 371:29-371:95 Type->Type testdata/Builtins.lc 371:29-371:95 Type testdata/Builtins.lc 371:30-371:47 Type testdata/Builtins.lc 371:30-371:47 Type->Type testdata/Builtins.lc 371:52-371:69 Type testdata/Builtins.lc 371:52-371:69 Type->Type testdata/Builtins.lc 371:74-371:91 Type testdata/Builtins.lc 371:74-371:91 Type->Type testdata/Builtins.lc 371:15-371:25 Type testdata/Builtins.lc 372:15-374:36 Type testdata/Builtins.lc 372:34-372:122 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 372:34-372:122 Type -> Type -> Type->Type testdata/Builtins.lc 372:34-372:122 Type -> Type->Type testdata/Builtins.lc 372:34-372:122 Type->Type testdata/Builtins.lc 372:34-372:122 Type testdata/Builtins.lc 372:35-372:52 Type testdata/Builtins.lc 372:35-372:52 Type->Type testdata/Builtins.lc 372:57-372:74 Type testdata/Builtins.lc 372:57-372:74 Type->Type testdata/Builtins.lc 372:79-372:96 Type testdata/Builtins.lc 372:79-372:96 Type->Type testdata/Builtins.lc 372:101-372:118 Type testdata/Builtins.lc 372:101-372:118 Type->Type testdata/Builtins.lc 372:15-372:29 Type testdata/Builtins.lc 373:15-374:36 Type testdata/Builtins.lc 373:38-373:148 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 373:38-373:148 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 373:38-373:148 Type -> Type -> Type->Type testdata/Builtins.lc 373:38-373:148 Type -> Type->Type testdata/Builtins.lc 373:38-373:148 Type->Type testdata/Builtins.lc 373:38-373:148 Type testdata/Builtins.lc 373:39-373:56 Type testdata/Builtins.lc 373:39-373:56 Type->Type testdata/Builtins.lc 373:61-373:78 Type testdata/Builtins.lc 373:61-373:78 Type->Type testdata/Builtins.lc 373:83-373:100 Type testdata/Builtins.lc 373:83-373:100 Type->Type testdata/Builtins.lc 373:105-373:122 Type testdata/Builtins.lc 373:105-373:122 Type->Type testdata/Builtins.lc 373:127-373:144 Type testdata/Builtins.lc 373:127-373:144 Type->Type testdata/Builtins.lc 373:15-373:33 Type testdata/Builtins.lc 374:19-374:36 Type testdata/Builtins.lc 374:19-374:36 Type->Type testdata/Builtins.lc 370:5-370:13 Type->Type testdata/Builtins.lc 376:6-376:12 Type->Type testdata/Builtins.lc 378:15-378:46 Type testdata/Builtins.lc 378:15-378:46 V3 testdata/Builtins.lc 378:15-378:46 V2 testdata/Builtins.lc 378:26-378:32 Type->Type testdata/Builtins.lc 378:38-378:44 Type->Type testdata/Builtins.lc 378:1-378:10 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 379:18-379:52 Type testdata/Builtins.lc 379:18-379:52 V1 testdata/Builtins.lc 379:23-379:27 Type testdata/Builtins.lc 379:32-379:38 Type->Type testdata/Builtins.lc 379:44-379:50 Type->Type testdata/Builtins.lc 379:1-379:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 381:22-381:35 Type testdata/Builtins.lc 381:6-381:15 'PrimitiveType -> Type->Type testdata/Builtins.lc 383:18-383:59 Type testdata/Builtins.lc 383:18-383:59 V5 testdata/Builtins.lc 383:18-383:59 V4 testdata/Builtins.lc 383:29-383:38 'PrimitiveType -> Type->Type testdata/Builtins.lc 383:18-383:59 'PrimitiveType testdata/Builtins.lc 383:18-383:59 V2 testdata/Builtins.lc 383:46-383:55 'PrimitiveType -> Type->Type testdata/Builtins.lc 383:1-383:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 385:39-385:96 Type testdata/Builtins.lc 385:39-385:53 {a} -> a->Type testdata/Builtins.lc 385:54-385:55 V0 testdata/Builtins.lc 385:54-385:55 V2 testdata/Builtins.lc 385:60-385:96 Type testdata/Builtins.lc 385:60-385:66 Type testdata/Builtins.lc 385:70-385:96 Type testdata/Builtins.lc 385:70-385:71 V3 testdata/Builtins.lc 385:75-385:96 Type testdata/Builtins.lc 385:75-385:81 Type->Type testdata/Builtins.lc 385:83-385:96 Type testdata/Builtins.lc 385:83-385:92 'PrimitiveType -> Type->Type testdata/Builtins.lc 385:93-385:94 'PrimitiveType testdata/Builtins.lc 385:93-385:94 V5 testdata/Builtins.lc 385:95-385:96 Type testdata/Builtins.lc 385:1-385:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 386:42-386:106 Type testdata/Builtins.lc 386:42-386:56 {a} -> a->Type testdata/Builtins.lc 386:57-386:58 V0 testdata/Builtins.lc 386:57-386:58 V4 testdata/Builtins.lc 386:60-386:106 Type testdata/Builtins.lc 386:60-386:61 Type testdata/Builtins.lc 386:60-386:61 V4 testdata/Builtins.lc 386:64-386:74 Type testdata/Builtins.lc 386:64-386:71 Type->Type testdata/Builtins.lc 386:72-386:74 Type testdata/Builtins.lc 386:72-386:74 V2 testdata/Builtins.lc 386:79-386:106 Type testdata/Builtins.lc 386:79-386:81 Type testdata/Builtins.lc 386:85-386:106 Type testdata/Builtins.lc 386:85-386:91 Type->Type testdata/Builtins.lc 386:93-386:106 Type testdata/Builtins.lc 386:93-386:102 'PrimitiveType -> Type->Type testdata/Builtins.lc 386:103-386:104 'PrimitiveType testdata/Builtins.lc 386:103-386:104 V6 testdata/Builtins.lc 386:105-386:106 Type testdata/Builtins.lc 386:1-386:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 388:19-388:79 Type testdata/Builtins.lc 388:19-388:79 V5 testdata/Builtins.lc 388:19-388:79 V4 testdata/Builtins.lc 388:31-388:37 Type->Type testdata/Builtins.lc 388:39-388:48 'PrimitiveType -> Type->Type testdata/Builtins.lc 388:19-388:79 'PrimitiveType testdata/Builtins.lc 388:19-388:79 V2 testdata/Builtins.lc 388:58-388:64 Type->Type testdata/Builtins.lc 388:66-388:75 'PrimitiveType -> Type->Type testdata/Builtins.lc 389:19-389:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 389:19-389:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) testdata/Builtins.lc 389:19-389:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) testdata/Builtins.lc 389:19-389:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 389:19-389:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 389:19-389:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 389:30-389:42 V1->V1 testdata/Builtins.lc 389:30-389:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 389:1-389:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 391:15-391:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 391:1-391:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) testdata/Builtins.lc 392:19-392:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 392:1-392:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) testdata/Builtins.lc 394:6-394:18 Type testdata/Builtins.lc 394:21-394:28 'DepthHandler testdata/Builtins.lc 394:31-394:43 'DepthHandler testdata/Builtins.lc 411:23-421:82 Type->Type testdata/Builtins.lc 411:23-421:82 Type testdata/Builtins.lc 411:23-411:25 Type testdata/Builtins.lc 412:25-421:82 Type testdata/Builtins.lc 412:25-412:26 Type testdata/Builtins.lc 413:19-421:82 Type testdata/Builtins.lc 413:39-413:45 Type -> Type->Type testdata/Builtins.lc 413:39-413:45 Type->Type testdata/Builtins.lc 413:39-413:45 Type testdata/Builtins.lc 413:19-413:35 Type testdata/Builtins.lc 414:19-421:82 Type testdata/Builtins.lc 414:48-419:58 Type -> Type -> Type->Type testdata/Builtins.lc 414:48-419:58 Type -> Type->Type testdata/Builtins.lc 414:48-419:58 Type->Type testdata/Builtins.lc 414:48-419:58 Type testdata/Builtins.lc 414:48-414:57 Type->Type testdata/Builtins.lc 414:48-414:57 Type testdata/Builtins.lc 414:48-414:57 Type -> Type -> Type->Type testdata/Builtins.lc 419:52-419:58 Type testdata/Builtins.lc 419:52-419:58 Type->Type testdata/Builtins.lc 419:52-419:58 Type -> Type->Type testdata/Builtins.lc 414:19-414:44 Type testdata/Builtins.lc 415:19-421:82 Type testdata/Builtins.lc 415:57-420:70 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 415:57-420:70 Type -> Type -> Type->Type testdata/Builtins.lc 415:57-420:70 Type -> Type->Type testdata/Builtins.lc 415:57-420:70 Type->Type testdata/Builtins.lc 415:57-420:70 Type testdata/Builtins.lc 415:57-415:69 Type->Type testdata/Builtins.lc 415:57-415:69 Type testdata/Builtins.lc 415:57-415:69 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 420:61-420:70 Type testdata/Builtins.lc 420:61-420:70 Type->Type testdata/Builtins.lc 420:61-420:70 Type -> Type -> Type->Type testdata/Builtins.lc 415:19-415:53 Type testdata/Builtins.lc 416:19-421:82 Type testdata/Builtins.lc 416:66-421:82 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 416:66-421:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 416:66-421:82 Type -> Type -> Type->Type testdata/Builtins.lc 416:66-421:82 Type -> Type->Type testdata/Builtins.lc 416:66-421:82 Type->Type testdata/Builtins.lc 416:66-421:82 Type testdata/Builtins.lc 416:66-416:81 Type->Type testdata/Builtins.lc 416:66-416:81 Type testdata/Builtins.lc 416:66-416:81 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 421:70-421:82 Type testdata/Builtins.lc 421:70-421:82 Type->Type testdata/Builtins.lc 421:70-421:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 416:19-416:62 Type testdata/Builtins.lc 417:25-417:36 Type testdata/Builtins.lc 417:34-417:36 Type->Type testdata/Builtins.lc 417:34-417:36 Type testdata/Builtins.lc 417:25-417:30 Type testdata/Builtins.lc 411:5-411:17 Type->Type testdata/Builtins.lc 425:18-425:21 Type testdata/Builtins.lc 425:25-425:53 Type testdata/Builtins.lc 425:25-425:37 Type testdata/Builtins.lc 425:41-425:53 Type testdata/Builtins.lc 425:41-425:45 Type testdata/Builtins.lc 425:49-425:53 Type testdata/Builtins.lc 425:6-425:14 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 427:20-427:78 Type testdata/Builtins.lc 427:20-427:78 V3 testdata/Builtins.lc 427:25-427:30 Type testdata/Builtins.lc 427:35-427:43 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 427:20-427:78 'Nat testdata/Builtins.lc 427:20-427:78 V2 testdata/Builtins.lc 427:53-427:61 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 427:64-427:76 'DepthHandler testdata/Builtins.lc 427:1-427:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 429:21-429:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 429:32-429:46 V1->V1 testdata/Builtins.lc 429:32-429:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 429:1-429:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) testdata/Builtins.lc 436:21-440:62 Type testdata/Builtins.lc 436:21-440:62 V7 testdata/Builtins.lc 436:25-436:41 Type->Type testdata/Builtins.lc 436:21-440:62 V5 testdata/Builtins.lc 436:21-440:62 V4 testdata/Builtins.lc 436:49-436:62 Type -> Type->Type testdata/Builtins.lc 436:64-436:75 Type testdata/Builtins.lc 436:64-436:67 'Nat -> Type->Type testdata/Builtins.lc 436:70-436:75 Type testdata/Builtins.lc 437:26-437:31 Type testdata/Builtins.lc 439:20-439:33 'PrimitiveType->Type testdata/Builtins.lc 436:21-440:62 'PrimitiveType testdata/Builtins.lc 440:20-440:29 'PrimitiveType -> Type->Type testdata/Builtins.lc 440:37-440:45 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 440:48-440:60 'DepthHandler testdata/Builtins.lc 436:1-436: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 testdata/Builtins.lc 442:20-442:56 Type testdata/Builtins.lc 442:20-442:56 V3 testdata/Builtins.lc 442:25-442:29 Type testdata/Builtins.lc 442:34-442:42 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 442:20-442:56 'Nat testdata/Builtins.lc 442:20-442:56 V2 testdata/Builtins.lc 442:52-442:56 Type testdata/Builtins.lc 442:1-442:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 444:21-444:84 Type testdata/Builtins.lc 444:21-444:84 V5 testdata/Builtins.lc 444:26-444:30 Type testdata/Builtins.lc 444:35-444:41 Type->Type testdata/Builtins.lc 444:43-444:51 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 444:21-444:84 'Nat testdata/Builtins.lc 444:21-444:84 V4 testdata/Builtins.lc 444:21-444:84 'DepthHandler testdata/Builtins.lc 444:21-444:84 V2 testdata/Builtins.lc 444:62-444:68 Type->Type testdata/Builtins.lc 444:70-444:78 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 445:21-445:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 445:21-445:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) testdata/Builtins.lc 445:21-445:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) testdata/Builtins.lc 445:21-445:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 445:21-445:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 445:21-445:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 445:35-445:49 V0->'Bool testdata/Builtins.lc 445:35-445:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 445:1-445:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 447:17-447:60 Type testdata/Builtins.lc 447:17-447:60 V7 testdata/Builtins.lc 447:17-447:60 V6 testdata/Builtins.lc 447:28-447:36 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 447:17-447:60 'Nat testdata/Builtins.lc 447:17-447:60 V4 testdata/Builtins.lc 447:17-447:60 'DepthHandler testdata/Builtins.lc 447:17-447:60 V2 testdata/Builtins.lc 447:46-447:54 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 447:1-447:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 449:18-449:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 449:29-449:40 V1->V1 testdata/Builtins.lc 449:29-449:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 449:1-449:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 454:13-454:26 Type->Type testdata/Builtins.lc 459:13-459:28 Type->Type testdata/Builtins.lc 462:10-463:36 V0->Type testdata/Builtins.lc 462:10-463:36 Type testdata/Builtins.lc 462:10-462:23 Type->Type testdata/Builtins.lc 462:10-462:23 Type testdata/Builtins.lc 462:10-462:23 Type -> 'Nat->Type testdata/Builtins.lc 462:10-462:23 'Nat->Type testdata/Builtins.lc 462:37-462:44 Type testdata/Builtins.lc 462:37-462:44 V1 testdata/Builtins.lc 463:10-463:36 Type testdata/Builtins.lc 463:10-463:23 Type->Type testdata/Builtins.lc 463:10-463:23 Type testdata/Builtins.lc 463:31-463:36 Type testdata/Builtins.lc 461:7-461:20 Type->Type testdata/Builtins.lc 461:7-461:65 Type testdata/Builtins.lc 461:46-461:65 Type testdata/Builtins.lc 461:46-461:63 Type->Type testdata/Builtins.lc 461:64-461:65 Type testdata/Builtins.lc 462:37-463:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a testdata/Builtins.lc 462:37-463:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 testdata/Builtins.lc 462:69-462:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) testdata/Builtins.lc 462:69-462:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) testdata/Builtins.lc 462:69-462:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) testdata/Builtins.lc 462:69-462:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) testdata/Builtins.lc 462:69-462:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) testdata/Builtins.lc 462:69-462:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) testdata/Builtins.lc 462:69-462:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a)))))) testdata/Builtins.lc 462:69-462:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) testdata/Builtins.lc 462:69-462:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) testdata/Builtins.lc 462:69-462: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) testdata/Builtins.lc 462:77-462:87 'Blending V1 testdata/Builtins.lc 462:77-462:87 {a} -> 'Blending a testdata/Builtins.lc 462:89-462:111 'VecScalar V2 'Bool testdata/Builtins.lc 462:89-462:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 462:92-462:96 V0 testdata/Builtins.lc 462:92-462:96 'Bool testdata/Builtins.lc 462:97-462:101 'Bool testdata/Builtins.lc 462:102-462:106 'Bool testdata/Builtins.lc 462:107-462:111 'Bool testdata/Builtins.lc 463:31-463:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 testdata/Builtins.lc 463:60-463:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) testdata/Builtins.lc 463:60-463:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) testdata/Builtins.lc 463:60-463:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 463:60-463:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 463:68-463:72 'ComparisonFunction testdata/Builtins.lc 463:73-463:77 'Bool testdata/Builtins.lc 461:29-461:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b testdata/Builtins.lc 470:24-470:27 Type testdata/Builtins.lc 470:6-470:17 'Nat -> Type->Type testdata/Builtins.lc 471:19-471:109 Type testdata/Builtins.lc 471:19-471:27 Type->Type testdata/Builtins.lc 471:28-471:29 Type testdata/Builtins.lc 471:33-471:39 Type->Type testdata/Builtins.lc 471:41-471:49 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 471:50-471:51 'Nat testdata/Builtins.lc 471:19-471:109 'DepthHandler testdata/Builtins.lc 471:19-471:109 V2 testdata/Builtins.lc 471:55-471:69 Type testdata/Builtins.lc 471:55-471:67 Type->Type testdata/Builtins.lc 471:68-471:69 Type testdata/Builtins.lc 471:75-471:109 Type testdata/Builtins.lc 471:75-471:86 'Nat -> Type->Type testdata/Builtins.lc 471:87-471:88 'Nat testdata/Builtins.lc 471:89-471:90 Type testdata/Builtins.lc 471:94-471:109 Type testdata/Builtins.lc 471:94-471:105 'Nat -> Type->Type testdata/Builtins.lc 471:106-471:107 'Nat testdata/Builtins.lc 471:108-471:109 Type testdata/Builtins.lc 471:3-471:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 472:20-472:117 Type testdata/Builtins.lc 472:20-472:36 {a} -> a->Type testdata/Builtins.lc 472:37-472:38 V0 testdata/Builtins.lc 472:37-472:38 Type testdata/Builtins.lc 472:40-472:55 Type->Type testdata/Builtins.lc 472:20-472:117 V2 testdata/Builtins.lc 472:59-472:74 Type testdata/Builtins.lc 472:59-472:70 'Nat -> Type->Type testdata/Builtins.lc 472:71-472:72 'Nat testdata/Builtins.lc 472:73-472:74 Type testdata/Builtins.lc 472:77-472:90 Type->Type testdata/Builtins.lc 472:102-472:117 Type testdata/Builtins.lc 472:102-472:113 'Nat -> Type->Type testdata/Builtins.lc 472:114-472:115 'Nat testdata/Builtins.lc 472:116-472:117 Type testdata/Builtins.lc 472:3-472:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 474:34-474:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 474:50-474:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) testdata/Builtins.lc 474:50-474:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 474:1-474:11 {a:'Nat} -> {b} -> {c:'DepthHandler} -> {d} -> 'FragOps' b -> (d -> 'RemSemantics b) -> 'Stream ('Fragment a c d) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 476:1-476:20 {a} -> a->a testdata/Builtins.lc 478:15-478:18 Type testdata/Builtins.lc 478:22-478:34 Type testdata/Builtins.lc 478:22-478:26 Type testdata/Builtins.lc 478:30-478:34 Type testdata/Builtins.lc 478:6-478:11 'Nat -> Type->Type testdata/Builtins.lc 479:48-480:56 Type testdata/Builtins.lc 479:48-479:51 Type->Type testdata/Builtins.lc 479:52-479:53 Type testdata/Builtins.lc 479:52-479:53 V3 testdata/Builtins.lc 479:55-480:56 Type testdata/Builtins.lc 479:55-479:60 Type testdata/Builtins.lc 479:55-479:60 V2 testdata/Builtins.lc 479:63-479:76 Type testdata/Builtins.lc 479:63-479:72 'Nat -> Type->Type testdata/Builtins.lc 479:73-479:74 'Nat testdata/Builtins.lc 479:73-479:74 V4 testdata/Builtins.lc 479:75-479:76 Type testdata/Builtins.lc 480:26-480:56 Type testdata/Builtins.lc 480:26-480:31 Type testdata/Builtins.lc 480:36-480:56 Type testdata/Builtins.lc 480:36-480:41 'Nat -> Type->Type testdata/Builtins.lc 480:42-480:43 'Nat testdata/Builtins.lc 480:42-480:43 V7 testdata/Builtins.lc 480:45-480:56 Type testdata/Builtins.lc 480:45-480:50 Type->Type testdata/Builtins.lc 480:51-480:56 Type testdata/Builtins.lc 479:3-479:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 481:37-481:67 Type testdata/Builtins.lc 481:37-481:42 Type testdata/Builtins.lc 481:47-481:67 Type testdata/Builtins.lc 481:47-481:52 'Nat -> Type->Type testdata/Builtins.lc 481:53-481:54 'Nat testdata/Builtins.lc 481:53-481:54 V2 testdata/Builtins.lc 481:56-481:67 Type testdata/Builtins.lc 481:56-481:61 Type->Type testdata/Builtins.lc 481:62-481:67 Type testdata/Builtins.lc 481:3-481:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 482:37-482:67 Type testdata/Builtins.lc 482:37-482:40 Type testdata/Builtins.lc 482:47-482:67 Type testdata/Builtins.lc 482:47-482:52 'Nat -> Type->Type testdata/Builtins.lc 482:53-482:54 'Nat testdata/Builtins.lc 482:53-482:54 V2 testdata/Builtins.lc 482:56-482:67 Type testdata/Builtins.lc 482:56-482:63 Type->Type testdata/Builtins.lc 482:64-482:67 Type testdata/Builtins.lc 482:3-482:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) testdata/Builtins.lc 485:26-485:54 Type testdata/Builtins.lc 485:26-485:37 'Nat -> Type->Type testdata/Builtins.lc 485:26-485:54 V1 testdata/Builtins.lc 485:45-485:50 'Nat -> Type->Type testdata/Builtins.lc 485:3-485:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a testdata/Builtins.lc 486:26-486:37 'Nat -> Type->Type testdata/Builtins.lc 486:40-486:74 Type testdata/Builtins.lc 486:40-486:74 Type -> Type->Type testdata/Builtins.lc 486:41-486:52 Type testdata/Builtins.lc 486:41-486:46 Type->Type testdata/Builtins.lc 486:47-486:52 Type testdata/Builtins.lc 486:54-486:72 Type testdata/Builtins.lc 486:54-486:59 Type->Type testdata/Builtins.lc 486:61-486:72 Type testdata/Builtins.lc 486:61-486:64 'Nat -> Type->Type testdata/Builtins.lc 486:67-486:72 Type testdata/Builtins.lc 486:78-486:105 Type testdata/Builtins.lc 486:78-486:83 'Nat -> Type->Type testdata/Builtins.lc 486:87-486:105 Type testdata/Builtins.lc 486:87-486:92 Type->Type testdata/Builtins.lc 486:94-486:105 Type testdata/Builtins.lc 486:94-486:97 'Nat -> Type->Type testdata/Builtins.lc 486:100-486:105 Type testdata/Builtins.lc 486:3-486: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)))))) testdata/Builtins.lc 480:42-486:105 Type testdata/Builtins.lc 480:42-480:56 Type testdata/Builtins.lc 481:53-486:105 Type testdata/Builtins.lc 481:53-481:67 Type testdata/Builtins.lc 482:53-486:105 Type testdata/Builtins.lc 482:53-482:67 Type testdata/Builtins.lc 485:26-486:105 Type testdata/Builtins.lc 488:6-488:12 Type testdata/Builtins.lc 489:26-489:51 Type testdata/Builtins.lc 489:26-489:37 'Nat -> Type->Type testdata/Builtins.lc 489:26-489:51 'Nat testdata/Builtins.lc 489:26-489:51 V3 testdata/Builtins.lc 489:26-489:51 V1 testdata/Builtins.lc 489:45-489:51 Type testdata/Builtins.lc 489:3-489:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 495:34-495:73 Type testdata/Builtins.lc 495:34-495:37 Type->Type testdata/Builtins.lc 495:39-495:55 Type->Type testdata/Builtins.lc 495:34-495:73 V1 testdata/Builtins.lc 495:1-495:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 495:10-495:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 495:19-495:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 496:35-496:80 Type testdata/Builtins.lc 496:35-496:80 V3 testdata/Builtins.lc 496:39-496:55 Type->Type testdata/Builtins.lc 496:35-496:80 V1 testdata/Builtins.lc 496:59-496:62 Type->Type testdata/Builtins.lc 496:1-496:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 496:11-496:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 496:21-496:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 497:35-497:75 Type testdata/Builtins.lc 497:35-497:38 Type->Type testdata/Builtins.lc 497:35-497:75 V5 testdata/Builtins.lc 497:35-497:75 V4 testdata/Builtins.lc 497:46-497:55 'Nat -> Type->Type testdata/Builtins.lc 497:35-497:75 'Nat testdata/Builtins.lc 497:35-497:75 V2 testdata/Builtins.lc 497:1-497:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 497:10-497:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 498:35-498:75 Type testdata/Builtins.lc 498:35-498:38 Type->Type testdata/Builtins.lc 498:35-498:75 V5 testdata/Builtins.lc 498:35-498:75 V4 testdata/Builtins.lc 498:46-498:55 'Nat -> Type->Type testdata/Builtins.lc 498:35-498:75 'Nat testdata/Builtins.lc 498:35-498:75 V2 testdata/Builtins.lc 498:1-498:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 498:11-498:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 499:34-499:71 Type testdata/Builtins.lc 499:34-499:40 Type->Type testdata/Builtins.lc 499:42-499:58 Type->Type testdata/Builtins.lc 499:34-499:71 V1 testdata/Builtins.lc 499:1-499:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a testdata/Builtins.lc 501:35-501:80 Type testdata/Builtins.lc 501:35-501:43 Type->Type testdata/Builtins.lc 501:35-501:80 V5 testdata/Builtins.lc 501:35-501:80 V4 testdata/Builtins.lc 501:51-501:60 'Nat -> Type->Type testdata/Builtins.lc 501:35-501:80 'Nat testdata/Builtins.lc 501:35-501:80 V2 testdata/Builtins.lc 501:1-501:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 501:11-501:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 501:20-501:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 502:35-502:80 Type testdata/Builtins.lc 502:35-502:43 Type->Type testdata/Builtins.lc 502:35-502:80 V5 testdata/Builtins.lc 502:35-502:80 V4 testdata/Builtins.lc 502:51-502:60 'Nat -> Type->Type testdata/Builtins.lc 502:35-502:80 'Nat testdata/Builtins.lc 502:35-502:80 V2 testdata/Builtins.lc 502:1-502:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 502:12-502:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 502:22-502:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 503:35-503:75 Type testdata/Builtins.lc 503:35-503:43 Type->Type testdata/Builtins.lc 503:35-503:75 V5 testdata/Builtins.lc 503:35-503:75 V4 testdata/Builtins.lc 503:51-503:60 'Nat -> Type->Type testdata/Builtins.lc 503:35-503:75 'Nat testdata/Builtins.lc 503:35-503:75 V2 testdata/Builtins.lc 503:1-503:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 504:35-504:102 Type testdata/Builtins.lc 504:35-504:43 Type->Type testdata/Builtins.lc 504:35-504:102 V7 testdata/Builtins.lc 504:35-504:102 V6 testdata/Builtins.lc 504:51-504:60 'Nat -> Type->Type testdata/Builtins.lc 504:35-504:102 'Nat testdata/Builtins.lc 504:35-504:102 V4 testdata/Builtins.lc 504:35-504:102 V3 testdata/Builtins.lc 504:70-504:79 'Nat -> Type->Type testdata/Builtins.lc 504:82-504:86 Type testdata/Builtins.lc 504:1-504:12 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b testdata/Builtins.lc 504:14-504:25 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b testdata/Builtins.lc 505:35-505:83 Type testdata/Builtins.lc 505:35-505:43 Type->Type testdata/Builtins.lc 505:35-505:83 V5 testdata/Builtins.lc 505:35-505:83 V4 testdata/Builtins.lc 505:51-505:60 'Nat -> Type->Type testdata/Builtins.lc 505:35-505:83 'Nat testdata/Builtins.lc 505:35-505:83 V2 testdata/Builtins.lc 505:74-505:78 Type testdata/Builtins.lc 505:1-505:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 505:15-505:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 507:34-507:38 Type testdata/Builtins.lc 507:42-507:54 Type testdata/Builtins.lc 507:42-507:46 Type testdata/Builtins.lc 507:50-507:54 Type testdata/Builtins.lc 507:1-507:8 'Bool -> 'Bool->'Bool testdata/Builtins.lc 507:10-507:16 'Bool -> 'Bool->'Bool testdata/Builtins.lc 507:18-507:25 'Bool -> 'Bool->'Bool testdata/Builtins.lc 508:35-508:66 Type testdata/Builtins.lc 508:35-508:66 V3 testdata/Builtins.lc 508:39-508:48 'Nat -> Type->Type testdata/Builtins.lc 508:35-508:66 'Nat testdata/Builtins.lc 508:35-508:66 V1 testdata/Builtins.lc 508:51-508:55 Type testdata/Builtins.lc 508:1-508:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a testdata/Builtins.lc 509:34-509:58 Type testdata/Builtins.lc 509:34-509:43 'Nat -> Type->Type testdata/Builtins.lc 509:34-509:58 'Nat testdata/Builtins.lc 509:34-509:58 V1 testdata/Builtins.lc 509:46-509:50 Type testdata/Builtins.lc 509:54-509:58 Type testdata/Builtins.lc 509:1-509:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 509:10-509:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 513:35-513:67 Type testdata/Builtins.lc 513:35-513:67 V3 testdata/Builtins.lc 513:39-513:48 'Nat -> Type->Type testdata/Builtins.lc 513:35-513:67 'Nat testdata/Builtins.lc 513:35-513:67 V1 testdata/Builtins.lc 513:51-513:56 Type testdata/Builtins.lc 512:1-512:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:11-512:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:22-512:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:32-512:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:43-512:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:53-512:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:64-512:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:73-512:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:83-512:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:96-512:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:109-512:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:118-512:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:128-512:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:137-512:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:147-512:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:156-512:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:165-512:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:175-512:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:185-512:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 512:195-512:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 514:35-514:72 Type testdata/Builtins.lc 514:35-514:72 V3 testdata/Builtins.lc 514:39-514:48 'Nat -> Type->Type testdata/Builtins.lc 514:35-514:72 'Nat testdata/Builtins.lc 514:35-514:72 V1 testdata/Builtins.lc 514:51-514:56 Type testdata/Builtins.lc 514:1-514:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 514:10-514:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 517:35-517:67 Type testdata/Builtins.lc 517:35-517:67 V3 testdata/Builtins.lc 517:39-517:48 'Nat -> Type->Type testdata/Builtins.lc 517:35-517:67 'Nat testdata/Builtins.lc 517:35-517:67 V1 testdata/Builtins.lc 517:51-517:56 Type testdata/Builtins.lc 516:1-516:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 516:12-516:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 516:23-516:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 516:34-516:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 516:49-516:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 516:59-516:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 518:35-518:75 Type testdata/Builtins.lc 518:35-518:38 Type->Type testdata/Builtins.lc 518:35-518:75 V5 testdata/Builtins.lc 518:35-518:75 V4 testdata/Builtins.lc 518:46-518:55 'Nat -> Type->Type testdata/Builtins.lc 518:35-518:75 'Nat testdata/Builtins.lc 518:35-518:75 V2 testdata/Builtins.lc 518:1-518:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 518:10-518:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 519:35-519:75 Type testdata/Builtins.lc 519:35-519:38 Type->Type testdata/Builtins.lc 519:35-519:75 V5 testdata/Builtins.lc 519:35-519:75 V4 testdata/Builtins.lc 519:46-519:55 'Nat -> Type->Type testdata/Builtins.lc 519:35-519:75 'Nat testdata/Builtins.lc 519:35-519:75 V2 testdata/Builtins.lc 519:1-519:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 519:11-519:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 520:35-520:89 Type testdata/Builtins.lc 520:35-520:89 V5 testdata/Builtins.lc 520:39-520:48 'Nat -> Type->Type testdata/Builtins.lc 520:35-520:89 'Nat testdata/Builtins.lc 520:35-520:89 V3 testdata/Builtins.lc 520:51-520:56 Type testdata/Builtins.lc 520:35-520:89 V2 testdata/Builtins.lc 520:62-520:71 'Nat -> Type->Type testdata/Builtins.lc 520:74-520:78 Type testdata/Builtins.lc 520:1-520:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 520:12-520:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 521:35-521:73 Type testdata/Builtins.lc 521:35-521:41 Type->Type testdata/Builtins.lc 521:35-521:73 V5 testdata/Builtins.lc 521:35-521:73 V4 testdata/Builtins.lc 521:49-521:58 'Nat -> Type->Type testdata/Builtins.lc 521:35-521:73 'Nat testdata/Builtins.lc 521:35-521:73 V2 testdata/Builtins.lc 521:1-521:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 521:10-521:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 522:35-522:72 Type testdata/Builtins.lc 522:35-522:72 V3 testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type testdata/Builtins.lc 522:35-522:72 'Nat testdata/Builtins.lc 522:35-522:72 V1 testdata/Builtins.lc 522:51-522:56 Type testdata/Builtins.lc 522:66-522:72 Type -> Type->Type testdata/Builtins.lc 522:1-522:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a testdata/Builtins.lc 523:35-523:80 Type testdata/Builtins.lc 523:35-523:38 Type->Type testdata/Builtins.lc 523:35-523:80 V5 testdata/Builtins.lc 523:35-523:80 V4 testdata/Builtins.lc 523:46-523:55 'Nat -> Type->Type testdata/Builtins.lc 523:35-523:80 'Nat testdata/Builtins.lc 523:35-523:80 V2 testdata/Builtins.lc 523:1-523:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b testdata/Builtins.lc 524:35-524:80 Type testdata/Builtins.lc 524:35-524:38 Type->Type testdata/Builtins.lc 524:35-524:80 V5 testdata/Builtins.lc 524:35-524:80 V4 testdata/Builtins.lc 524:46-524:55 'Nat -> Type->Type testdata/Builtins.lc 524:35-524:80 'Nat testdata/Builtins.lc 524:35-524:80 V2 testdata/Builtins.lc 524:1-524:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b testdata/Builtins.lc 525:35-525:77 Type testdata/Builtins.lc 525:35-525:77 V3 testdata/Builtins.lc 525:39-525:48 'Nat -> Type->Type testdata/Builtins.lc 525:35-525:77 'Nat testdata/Builtins.lc 525:35-525:77 V1 testdata/Builtins.lc 525:51-525:56 Type testdata/Builtins.lc 525:1-525:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 526:35-526:81 Type testdata/Builtins.lc 526:35-526:81 V3 testdata/Builtins.lc 526:39-526:48 'Nat -> Type->Type testdata/Builtins.lc 526:35-526:81 'Nat testdata/Builtins.lc 526:35-526:81 V1 testdata/Builtins.lc 526:51-526:56 Type testdata/Builtins.lc 526:71-526:76 Type testdata/Builtins.lc 526:1-526:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a testdata/Builtins.lc 527:35-527:99 Type testdata/Builtins.lc 527:35-527:99 V5 testdata/Builtins.lc 527:39-527:48 'Nat -> Type->Type testdata/Builtins.lc 527:35-527:99 'Nat testdata/Builtins.lc 527:35-527:99 V3 testdata/Builtins.lc 527:51-527:56 Type testdata/Builtins.lc 527:35-527:99 V2 testdata/Builtins.lc 527:62-527:71 'Nat -> Type->Type testdata/Builtins.lc 527:74-527:78 Type testdata/Builtins.lc 527:1-527:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a testdata/Builtins.lc 528:35-528:68 Type testdata/Builtins.lc 528:35-528:68 V3 testdata/Builtins.lc 528:39-528:44 'Nat -> Type->Type testdata/Builtins.lc 528:35-528:68 'Nat testdata/Builtins.lc 528:35-528:68 V1 testdata/Builtins.lc 528:47-528:52 Type testdata/Builtins.lc 528:1-528:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a testdata/Builtins.lc 529:35-529:76 Type testdata/Builtins.lc 529:35-529:76 V3 testdata/Builtins.lc 529:39-529:48 'Nat -> Type->Type testdata/Builtins.lc 529:35-529:76 'Nat testdata/Builtins.lc 529:35-529:76 V1 testdata/Builtins.lc 529:51-529:56 Type testdata/Builtins.lc 529:61-529:66 Type testdata/Builtins.lc 529:1-529:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a testdata/Builtins.lc 530:35-530:73 Type testdata/Builtins.lc 530:35-530:73 V3 testdata/Builtins.lc 530:39-530:44 'Nat -> Type->Type testdata/Builtins.lc 530:35-530:73 'Nat testdata/Builtins.lc 530:35-530:73 V1 testdata/Builtins.lc 530:47-530:52 Type testdata/Builtins.lc 530:1-530:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a testdata/Builtins.lc 531:35-531:85 Type testdata/Builtins.lc 531:35-531:85 V3 testdata/Builtins.lc 531:39-531:48 'Nat -> Type->Type testdata/Builtins.lc 531:35-531:85 'Nat testdata/Builtins.lc 531:35-531:85 V1 testdata/Builtins.lc 531:51-531:56 Type testdata/Builtins.lc 531:61-531:66 Type testdata/Builtins.lc 531:70-531:75 Type testdata/Builtins.lc 531:1-531:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a testdata/Builtins.lc 534:34-534:70 Type testdata/Builtins.lc 534:34-534:43 'Nat -> Type->Type testdata/Builtins.lc 534:34-534:70 'Nat testdata/Builtins.lc 534:34-534:70 V1 testdata/Builtins.lc 534:46-534:51 Type testdata/Builtins.lc 534:55-534:64 'Nat -> Type->Type testdata/Builtins.lc 534:67-534:70 Type testdata/Builtins.lc 534:1-534:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int testdata/Builtins.lc 535:34-535:71 Type testdata/Builtins.lc 535:34-535:43 'Nat -> Type->Type testdata/Builtins.lc 535:34-535:71 'Nat testdata/Builtins.lc 535:34-535:71 V1 testdata/Builtins.lc 535:46-535:51 Type testdata/Builtins.lc 535:55-535:64 'Nat -> Type->Type testdata/Builtins.lc 535:67-535:71 Type testdata/Builtins.lc 535:1-535:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word testdata/Builtins.lc 536:34-536:72 Type testdata/Builtins.lc 536:34-536:43 'Nat -> Type->Type testdata/Builtins.lc 536:34-536:72 'Nat testdata/Builtins.lc 536:34-536:72 V1 testdata/Builtins.lc 536:46-536:49 Type testdata/Builtins.lc 536:55-536:64 'Nat -> Type->Type testdata/Builtins.lc 536:67-536:72 Type testdata/Builtins.lc 536:1-536:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float testdata/Builtins.lc 537:34-537:72 Type testdata/Builtins.lc 537:34-537:43 'Nat -> Type->Type testdata/Builtins.lc 537:34-537:72 'Nat testdata/Builtins.lc 537:34-537:72 V1 testdata/Builtins.lc 537:46-537:50 Type testdata/Builtins.lc 537:55-537:64 'Nat -> Type->Type testdata/Builtins.lc 537:67-537:72 Type testdata/Builtins.lc 537:1-537:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float testdata/Builtins.lc 539:35-539:71 Type testdata/Builtins.lc 539:35-539:71 V3 testdata/Builtins.lc 539:39-539:48 'Nat -> Type->Type testdata/Builtins.lc 539:35-539:71 'Nat testdata/Builtins.lc 539:35-539:71 V1 testdata/Builtins.lc 539:51-539:56 Type testdata/Builtins.lc 539:66-539:71 Type testdata/Builtins.lc 539:1-539:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float testdata/Builtins.lc 540:35-540:76 Type testdata/Builtins.lc 540:35-540:76 V3 testdata/Builtins.lc 540:39-540:48 'Nat -> Type->Type testdata/Builtins.lc 540:35-540:76 'Nat testdata/Builtins.lc 540:35-540:76 V1 testdata/Builtins.lc 540:51-540:56 Type testdata/Builtins.lc 540:71-540:76 Type testdata/Builtins.lc 540:1-540:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 540:15-540:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 541:35-541:72 Type testdata/Builtins.lc 541:35-541:72 V1 testdata/Builtins.lc 541:39-541:56 Type testdata/Builtins.lc 541:39-541:48 'Nat -> Type->Type testdata/Builtins.lc 541:51-541:56 Type testdata/Builtins.lc 541:1-541:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a testdata/Builtins.lc 542:35-542:67 Type testdata/Builtins.lc 542:35-542:67 V3 testdata/Builtins.lc 542:39-542:48 'Nat -> Type->Type testdata/Builtins.lc 542:35-542:67 'Nat testdata/Builtins.lc 542:35-542:67 V1 testdata/Builtins.lc 542:51-542:56 Type testdata/Builtins.lc 542:1-542:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 543:35-543:77 Type testdata/Builtins.lc 543:35-543:77 V3 testdata/Builtins.lc 543:39-543:48 'Nat -> Type->Type testdata/Builtins.lc 543:35-543:77 'Nat testdata/Builtins.lc 543:35-543:77 V1 testdata/Builtins.lc 543:51-543:56 Type testdata/Builtins.lc 543:1-543:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 543:18-543:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 544:35-544:72 Type testdata/Builtins.lc 544:35-544:72 V3 testdata/Builtins.lc 544:39-544:48 'Nat -> Type->Type testdata/Builtins.lc 544:35-544:72 'Nat testdata/Builtins.lc 544:35-544:72 V1 testdata/Builtins.lc 544:51-544:56 Type testdata/Builtins.lc 544:1-544:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 546:34-546:57 Type testdata/Builtins.lc 546:34-546:39 Type -> Type->Type testdata/Builtins.lc 546:34-546:57 V3 testdata/Builtins.lc 546:34-546:57 V1 testdata/Builtins.lc 546:48-546:53 Type -> Type->Type testdata/Builtins.lc 546:1-546:14 {a} -> {b} -> 'TFMat a b -> 'TFMat b a testdata/Builtins.lc 547:34-547:53 Type testdata/Builtins.lc 547:34-547:39 Type -> Type->Type testdata/Builtins.lc 547:34-547:53 V1 testdata/Builtins.lc 547:48-547:53 Type testdata/Builtins.lc 547:1-547:16 {a} -> 'TFMat a a -> 'Float testdata/Builtins.lc 548:34-548:57 Type testdata/Builtins.lc 548:34-548:39 Type -> Type->Type testdata/Builtins.lc 548:34-548:57 V1 testdata/Builtins.lc 548:48-548:53 Type -> Type->Type testdata/Builtins.lc 548:1-548:12 {a} -> 'TFMat a a -> 'TFMat a a testdata/Builtins.lc 549:34-549:71 Type testdata/Builtins.lc 549:34-549:71 V3 testdata/Builtins.lc 549:34-549:71 V2 testdata/Builtins.lc 549:62-549:67 Type -> Type->Type testdata/Builtins.lc 549:1-549:17 {a} -> {b} -> a -> b -> 'TFMat b a testdata/Builtins.lc 550:34-550:63 Type testdata/Builtins.lc 550:34-550:39 Type -> Type->Type testdata/Builtins.lc 550:34-550:63 V3 testdata/Builtins.lc 550:34-550:63 V1 testdata/Builtins.lc 550:1-550:14 {a} -> {b} -> 'TFMat a b -> b->a testdata/Builtins.lc 551:34-551:63 Type testdata/Builtins.lc 551:34-551:63 V3 testdata/Builtins.lc 551:48-551:53 Type -> Type->Type testdata/Builtins.lc 551:34-551:63 V2 testdata/Builtins.lc 551:1-551:14 {a} -> {b} -> a -> 'TFMat a b -> b testdata/Builtins.lc 552:34-552:71 Type testdata/Builtins.lc 552:34-552:39 Type -> Type->Type testdata/Builtins.lc 552:34-552:71 V5 testdata/Builtins.lc 552:34-552:71 V3 testdata/Builtins.lc 552:48-552:53 Type -> Type->Type testdata/Builtins.lc 552:34-552:71 V2 testdata/Builtins.lc 552:62-552:67 Type -> Type->Type testdata/Builtins.lc 552:1-552:14 {a} -> {b} -> {c} -> 'TFMat a b -> 'TFMat b c -> 'TFMat a c testdata/Builtins.lc 555:35-555:97 Type testdata/Builtins.lc 555:35-555:38 Type->Type testdata/Builtins.lc 555:35-555:97 V7 testdata/Builtins.lc 555:35-555:97 V6 testdata/Builtins.lc 555:46-555:55 'Nat -> Type->Type testdata/Builtins.lc 555:35-555:97 'Nat testdata/Builtins.lc 555:35-555:97 V4 testdata/Builtins.lc 555:35-555:97 V3 testdata/Builtins.lc 555:65-555:74 'Nat -> Type->Type testdata/Builtins.lc 555:77-555:81 Type testdata/Builtins.lc 554:1-554:13 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 554:15-554:32 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 554:34-554:49 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 554:51-554:71 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 554:73-554:83 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 554:85-554:98 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 556:35-556:76 Type testdata/Builtins.lc 556:35-556:76 V3 testdata/Builtins.lc 556:39-556:55 Type->Type testdata/Builtins.lc 556:35-556:76 V1 testdata/Builtins.lc 556:72-556:76 Type testdata/Builtins.lc 556:1-556:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 556:12-556:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 559:35-559:67 Type testdata/Builtins.lc 559:35-559:67 V3 testdata/Builtins.lc 559:39-559:48 'Nat -> Type->Type testdata/Builtins.lc 559:35-559:67 'Nat testdata/Builtins.lc 559:35-559:67 V1 testdata/Builtins.lc 559:51-559:56 Type testdata/Builtins.lc 558:1-558:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 558:11-558:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 558:21-558:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 561:34-561:60 Type testdata/Builtins.lc 561:34-561:43 'Nat -> Type->Type testdata/Builtins.lc 561:34-561:60 'Nat testdata/Builtins.lc 561:34-561:60 V1 testdata/Builtins.lc 561:46-561:51 Type testdata/Builtins.lc 561:55-561:60 Type testdata/Builtins.lc 561:1-561:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float testdata/Builtins.lc 562:34-562:66 Type testdata/Builtins.lc 562:34-562:43 'Nat -> Type->Type testdata/Builtins.lc 562:34-562:66 'Nat testdata/Builtins.lc 562:34-562:66 V1 testdata/Builtins.lc 562:46-562:51 Type testdata/Builtins.lc 562:55-562:66 Type testdata/Builtins.lc 562:55-562:58 'Nat -> Type->Type testdata/Builtins.lc 562:61-562:66 Type testdata/Builtins.lc 562:1-562:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 563:34-563:66 Type testdata/Builtins.lc 563:34-563:43 'Nat -> Type->Type testdata/Builtins.lc 563:34-563:66 'Nat testdata/Builtins.lc 563:34-563:66 V1 testdata/Builtins.lc 563:46-563:51 Type testdata/Builtins.lc 563:55-563:66 Type testdata/Builtins.lc 563:55-563:58 'Nat -> Type->Type testdata/Builtins.lc 563:61-563:66 Type testdata/Builtins.lc 563:1-563:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 564:34-564:66 Type testdata/Builtins.lc 564:34-564:43 'Nat -> Type->Type testdata/Builtins.lc 564:34-564:66 'Nat testdata/Builtins.lc 564:34-564:66 V1 testdata/Builtins.lc 564:46-564:51 Type testdata/Builtins.lc 564:55-564:66 Type testdata/Builtins.lc 564:55-564:58 'Nat -> Type->Type testdata/Builtins.lc 564:61-564:66 Type testdata/Builtins.lc 564:1-564:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 580:6-580:13 Type testdata/Builtins.lc 581:20-581:26 Type testdata/Builtins.lc 582:20-582:27 Type testdata/Builtins.lc 581:3-581:16 'String->'Texture testdata/Builtins.lc 584:20-584:23 'Nat -> Type->Type testdata/Builtins.lc 584:26-584:29 Type testdata/Builtins.lc 585:20-586:27 Type testdata/Builtins.lc 585:20-585:25 'Nat -> Type->Type testdata/Builtins.lc 585:29-585:47 Type testdata/Builtins.lc 585:29-585:34 Type->Type testdata/Builtins.lc 585:36-585:47 Type testdata/Builtins.lc 585:36-585:39 'Nat -> Type->Type testdata/Builtins.lc 585:42-585:47 Type testdata/Builtins.lc 586:20-586:27 Type testdata/Builtins.lc 584:3-584:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture testdata/Builtins.lc 588:6-588:12 Type testdata/Builtins.lc 589:5-589:16 'Filter testdata/Builtins.lc 590:5-590:17 'Filter testdata/Builtins.lc 592:6-592:14 Type testdata/Builtins.lc 593:5-593:11 'EdgeMode testdata/Builtins.lc 594:5-594:19 'EdgeMode testdata/Builtins.lc 595:5-595:16 'EdgeMode testdata/Builtins.lc 597:6-597:13 Type testdata/Builtins.lc 597:24-597:30 Type testdata/Builtins.lc 597:6-597:47 Type testdata/Builtins.lc 597:31-597:39 Type testdata/Builtins.lc 597:40-597:47 Type testdata/Builtins.lc 597:16-597:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler testdata/Builtins.lc 600:14-600:21 Type testdata/Builtins.lc 600:25-600:51 Type testdata/Builtins.lc 600:25-600:28 'Nat -> Type->Type testdata/Builtins.lc 600:31-600:36 Type testdata/Builtins.lc 600:40-600:51 Type testdata/Builtins.lc 600:40-600:43 'Nat -> Type->Type testdata/Builtins.lc 600:46-600:51 Type testdata/Builtins.lc 600:1-600:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 603:30-603:39 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 603:41-603:60 V1->V1 testdata/Builtins.lc 603:41-603: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 testdata/Builtins.lc 603:53-603:60 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float testdata/Builtins.lc 603:59-603:60 'Float testdata/Builtins.lc 603:59-603:60 'Int testdata/Builtins.lc 603:1-603: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)) testdata/Builtins.lc 604:46-604:55 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 604:57-604:67 V1->V1 testdata/Builtins.lc 604:57-604: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 testdata/Builtins.lc 604:1-604: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)) testdata/Builtins.lc 605:24-605:32 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 605:1-605:15 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 606:25-606:35 V2 -> V2->V2 testdata/Builtins.lc 606:25-606:35 V2->V2 testdata/Builtins.lc 606:25-606:35 V2 testdata/Builtins.lc 606:25-606:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 606:13-606:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) testdata/Builtins.lc 606:13-606:21 V4 testdata/Builtins.lc 606:1-606:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b testdata/Builtins.lc 607:15-607:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 607:1-607:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 608:14-608:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 608:1-608:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 609:19-609:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 609:1-609:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) testdata/Builtins.lc 610:19-610:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 610:1-610:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c)