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 120:10-166:19 V0->Type testdata/Builtins.lc 120:10-166:19 Type testdata/Builtins.lc 120:10-120:19 Type testdata/Builtins.lc 120:20-120:24 Type testdata/Builtins.lc 120:20-120:24 V1 testdata/Builtins.lc 126:10-166:19 Type testdata/Builtins.lc 126:10-126:19 Type testdata/Builtins.lc 126:20-126:23 Type testdata/Builtins.lc 133:10-166:19 Type testdata/Builtins.lc 133:10-133:19 Type testdata/Builtins.lc 133:20-133:24 Type testdata/Builtins.lc 140:10-166:19 Type testdata/Builtins.lc 140:10-140:19 Type testdata/Builtins.lc 140:20-140:25 Type testdata/Builtins.lc 146:10-166:19 Type testdata/Builtins.lc 146:10-166:19 Type -> 'Nat->Type testdata/Builtins.lc 146:10-166:19 'Nat->Type testdata/Builtins.lc 146:10-158:19 Type testdata/Builtins.lc 146:10-158:19 'Nat->Type testdata/Builtins.lc 146:10-146:19 Type testdata/Builtins.lc 152:10-158:19 'Nat->Type testdata/Builtins.lc 152:10-158:19 Type testdata/Builtins.lc 152:10-152:19 Type testdata/Builtins.lc 158:10-158:19 'Nat->Type testdata/Builtins.lc 158:10-158:19 Type testdata/Builtins.lc 164:10-166:19 Type testdata/Builtins.lc 164:10-166:19 'Nat->Type testdata/Builtins.lc 164:10-164:19 Type testdata/Builtins.lc 165:10-166:19 'Nat->Type testdata/Builtins.lc 165:10-166:19 Type testdata/Builtins.lc 165:10-165:19 Type testdata/Builtins.lc 166:10-166:19 'Nat->Type testdata/Builtins.lc 166:10-166:19 Type testdata/Builtins.lc 146:26-146:33 Type testdata/Builtins.lc 112:7-112:16 Type->Type testdata/Builtins.lc 112:7-113:28 Type testdata/Builtins.lc 113:11-113:28 Type testdata/Builtins.lc 113:11-113:12 Type testdata/Builtins.lc 113:16-113:28 Type testdata/Builtins.lc 113:16-113:17 Type testdata/Builtins.lc 113:21-113:28 Type testdata/Builtins.lc 113:21-113:24 'Nat -> Type->Type testdata/Builtins.lc 113:27-113:28 Type testdata/Builtins.lc 120:20-167:12 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 120:20-167:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 121:10-121:12 {a:'Unit} -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 121:10-121:12 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 121:10-121:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 126:20-167:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 127:10-127:12 {a:'Unit} -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 127:10-127:12 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 127:10-127:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 133:20-167:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 134:10-134:12 {a:'Unit} -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 134:10-134:12 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 134:10-134:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 140:20-167:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 141:10-141:12 {a:'Unit} -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 141:10-141:12 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 141:10-141:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 146:26-167:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 147:10-167: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 147:10-167:12 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a -> 'VecS V3 a -> 'VecS ('VecS V4 a) (Succ (Succ Zero)) testdata/Builtins.lc 147:10-167:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 147:10-159:12 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 -> 'VecS 'Float V2 -> 'VecS ('VecS 'Float V3) (Succ (Succ Zero)) testdata/Builtins.lc 147:10-159: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 147:10-159: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 147:10-159: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 147:10-159: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 147:10-147: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 147:10-147:12 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ Zero)) testdata/Builtins.lc 147:10-147:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 153:10-159: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 153:10-159: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 153:10-153: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 153:10-153: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 153:10-153:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 159:10-159: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 159:10-159: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 159:10-159: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 159:10-159: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 159:10-159:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 167:10-167:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 167:10-167:12 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 -> 'VecS 'Bool V2 -> 'VecS ('VecS 'Bool V3) (Succ (Succ Zero)) testdata/Builtins.lc 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167: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 167:10-167:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 113:3-113:7 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 112:7-114:33 Type testdata/Builtins.lc 114:11-114:33 Type testdata/Builtins.lc 114:11-114:12 Type testdata/Builtins.lc 114:16-114:33 Type testdata/Builtins.lc 114:16-114:17 Type testdata/Builtins.lc 114:21-114:33 Type testdata/Builtins.lc 114:21-114:22 Type testdata/Builtins.lc 114:26-114:33 Type testdata/Builtins.lc 114:26-114:29 'Nat -> Type->Type testdata/Builtins.lc 114:32-114:33 Type testdata/Builtins.lc 120:20-168:12 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 120:20-168:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 122:10-122:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 122:10-122:12 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 122:10-122:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 126:20-168:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 128:10-128:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 128:10-128:12 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 128:10-128:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 133:20-168:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 135:10-135:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 135:10-135:12 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 135:10-135:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 140:20-168:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 142:10-142:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 142:10-142:12 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 142:10-142:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 146:26-168:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 148:10-168: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 148:10-168: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 148:10-168: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 148:10-160: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 148:10-160: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 148:10-160: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 148:10-160: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 148:10-160: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 148:10-148: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 148:10-148: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 148:10-148:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 154:10-160: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 154:10-160: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 154:10-154: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 154:10-154: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 154:10-154:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 160:10-160: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 160:10-160: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 160:10-160: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 160:10-160: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 160:10-160:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168: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 168:10-168:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 114:3-114:7 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 112:7-115:38 Type testdata/Builtins.lc 115:11-115:38 Type testdata/Builtins.lc 115:11-115:12 Type testdata/Builtins.lc 115:16-115:38 Type testdata/Builtins.lc 115:16-115:17 Type testdata/Builtins.lc 115:21-115:38 Type testdata/Builtins.lc 115:21-115:22 Type testdata/Builtins.lc 115:26-115:38 Type testdata/Builtins.lc 115:26-115:27 Type testdata/Builtins.lc 115:31-115:38 Type testdata/Builtins.lc 115:31-115:34 'Nat -> Type->Type testdata/Builtins.lc 115:37-115:38 Type testdata/Builtins.lc 120:20-169:12 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 120:20-169:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 123:10-123:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 123:10-123:12 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 123:10-123:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 126:20-169:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 129:10-129:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 129:10-129:12 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 129:10-129:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 133:20-169:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 136:10-136:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 136:10-136:12 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 136:10-136:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 140:20-169:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 143:10-143:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 143:10-143:12 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 143:10-143:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 146:26-169:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 149:10-169: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 149:10-169: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 149:10-169: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 149:10-161: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 149:10-161: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 149:10-161: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 149:10-161: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 149:10-161: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 149:10-149: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 149:10-149: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 149:10-149:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 155:10-161: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 155:10-161: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 155:10-155: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 155:10-155: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 155:10-155:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 161:10-161: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 161:10-161: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 161:10-161: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 161:10-161: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 161:10-161:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169: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 169:10-169:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 115:3-115:7 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 112:7-116:16 Type testdata/Builtins.lc 116:15-116:16 Type testdata/Builtins.lc 120:20-170:40 {a} -> {b : 'Component a}->a testdata/Builtins.lc 120:20-170:40 {a : 'Component V0}->V1 testdata/Builtins.lc 124:14-124:19 {a:'Unit}->'Bool testdata/Builtins.lc 124:14-124:19 'Bool testdata/Builtins.lc 126:20-170:40 {a : 'Component V0}->V1 testdata/Builtins.lc 130:14-130:22 {a:'Unit}->'Int testdata/Builtins.lc 130:19-130:22 Type testdata/Builtins.lc 130:14-130:15 'Int testdata/Builtins.lc 133:20-170:40 {a : 'Component V0}->V1 testdata/Builtins.lc 137:14-137:23 {a:'Unit}->'Word testdata/Builtins.lc 137:19-137:23 Type testdata/Builtins.lc 137:14-137:15 'Word testdata/Builtins.lc 137:14-137:15 'Int testdata/Builtins.lc 140:20-170:40 {a : 'Component V0}->V1 testdata/Builtins.lc 144:14-144:17 {a:'Unit}->'Float testdata/Builtins.lc 144:14-144:17 'Float testdata/Builtins.lc 146:26-170:40 {a : 'Component V0}->V1 testdata/Builtins.lc 150:14-170:40 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 150:14-170:40 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 150:14-170:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 150:14-162:32 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 150:14-162:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 150:14-162:32 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 150:14-162:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 150:14-162:32 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 150:14-150:24 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 150:14-150:16 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 150:17-150:20 V0 testdata/Builtins.lc 150:17-150:20 'Float testdata/Builtins.lc 150:21-150:24 'Float testdata/Builtins.lc 156:14-162:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 156:14-162:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 156:14-156:28 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 156:14-156:16 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 156:17-156:20 V0 testdata/Builtins.lc 156:17-156:20 'Float testdata/Builtins.lc 156:21-156:24 'Float testdata/Builtins.lc 156:25-156:28 'Float testdata/Builtins.lc 162:14-162:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 162:14-162:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 162:14-162:32 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 162:14-162:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 162:17-162:20 V0 testdata/Builtins.lc 162:17-162:20 'Float testdata/Builtins.lc 162:21-162:24 'Float testdata/Builtins.lc 162:25-162:28 'Float testdata/Builtins.lc 162:29-162:32 'Float testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 170:14-170:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 170:14-170:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 170:14-170:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 170:14-170:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 170:14-170:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 170:14-170:40 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 170:14-170:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 170:17-170:22 V0 testdata/Builtins.lc 170:17-170:22 'Bool testdata/Builtins.lc 170:23-170:28 'Bool testdata/Builtins.lc 170:29-170:34 'Bool testdata/Builtins.lc 170:35-170:40 'Bool testdata/Builtins.lc 116:3-116:11 {a} -> {b : 'Component a}->a testdata/Builtins.lc 112:7-117:15 Type testdata/Builtins.lc 117:14-117:15 Type testdata/Builtins.lc 120:20-171:35 {a} -> {b : 'Component a}->a testdata/Builtins.lc 120:20-171:35 {a : 'Component V0}->V1 testdata/Builtins.lc 125:13-125:17 {a:'Unit}->'Bool testdata/Builtins.lc 125:13-125:17 'Bool testdata/Builtins.lc 126:20-171:35 {a : 'Component V0}->V1 testdata/Builtins.lc 131:13-131:21 {a:'Unit}->'Int testdata/Builtins.lc 131:18-131:21 Type testdata/Builtins.lc 131:13-131:14 'Int testdata/Builtins.lc 133:20-171:35 {a : 'Component V0}->V1 testdata/Builtins.lc 138:13-138:22 {a:'Unit}->'Word testdata/Builtins.lc 138:18-138:22 Type testdata/Builtins.lc 138:13-138:14 'Word testdata/Builtins.lc 138:13-138:14 'Int testdata/Builtins.lc 140:20-171:35 {a : 'Component V0}->V1 testdata/Builtins.lc 145:13-145:16 {a:'Unit}->'Float testdata/Builtins.lc 145:13-145:16 'Float testdata/Builtins.lc 146:26-171:35 {a : 'Component V0}->V1 testdata/Builtins.lc 151:13-171:35 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 151:13-171:35 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 151:13-171:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 151:13-163:31 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 151:13-163:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 151:13-163:31 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 151:13-163:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 151:13-163:31 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 151:13-151:23 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 151:13-151:15 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 151:16-151:19 V0 testdata/Builtins.lc 151:16-151:19 'Float testdata/Builtins.lc 151:20-151:23 'Float testdata/Builtins.lc 157:13-163:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 157:13-163:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 157:13-157:27 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 157:13-157:15 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 157:16-157:19 V0 testdata/Builtins.lc 157:16-157:19 'Float testdata/Builtins.lc 157:20-157:23 'Float testdata/Builtins.lc 157:24-157:27 'Float testdata/Builtins.lc 163:13-163:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 163:13-163:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 163:13-163:31 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 163:13-163:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 163:16-163:19 V0 testdata/Builtins.lc 163:16-163:19 'Float testdata/Builtins.lc 163:20-163:23 'Float testdata/Builtins.lc 163:24-163:27 'Float testdata/Builtins.lc 163:28-163:31 'Float testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 171:13-171:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 171:13-171:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 171:13-171:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 171:13-171:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 171:13-171:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 171:13-171:35 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 171:13-171:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 171:16-171:20 V0 testdata/Builtins.lc 171:16-171:20 'Bool testdata/Builtins.lc 171:21-171:25 'Bool testdata/Builtins.lc 171:26-171:30 'Bool testdata/Builtins.lc 171:31-171:35 'Bool testdata/Builtins.lc 117:3-117:10 {a} -> {b : 'Component a}->a testdata/Builtins.lc 175:10-176:29 V0->Type testdata/Builtins.lc 175:10-176:29 Type testdata/Builtins.lc 175:10-175:18 Type testdata/Builtins.lc 175:25-175:28 Type testdata/Builtins.lc 175:25-175:28 V1 testdata/Builtins.lc 176:10-176:29 Type testdata/Builtins.lc 176:10-176:18 Type testdata/Builtins.lc 176:25-176:29 Type testdata/Builtins.lc 173:7-173:15 Type->Type testdata/Builtins.lc 180:10-192:18 V0->Type testdata/Builtins.lc 180:10-192:18 Type testdata/Builtins.lc 180:10-180:18 Type testdata/Builtins.lc 180:25-180:30 Type testdata/Builtins.lc 180:25-180:30 V1 testdata/Builtins.lc 181:10-192:18 Type testdata/Builtins.lc 181:10-183:18 Type -> 'Nat->Type testdata/Builtins.lc 181:10-183:18 'Nat->Type testdata/Builtins.lc 181:10-183:18 Type testdata/Builtins.lc 181:10-181:18 Type testdata/Builtins.lc 182:10-183:18 'Nat->Type testdata/Builtins.lc 182:10-183:18 Type testdata/Builtins.lc 182:10-182:18 Type testdata/Builtins.lc 183:10-183:18 'Nat->Type testdata/Builtins.lc 183:10-183:18 Type testdata/Builtins.lc 181:31-181:38 Type testdata/Builtins.lc 184:10-192:18 Type testdata/Builtins.lc 184:10-192:18 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 184:10-192:18 'Nat -> Type->Type testdata/Builtins.lc 184:10-192:18 Type->Type testdata/Builtins.lc 184:10-192:18 'Nat->Type testdata/Builtins.lc 184:10-186:18 Type testdata/Builtins.lc 184:10-186:18 'Nat->Type testdata/Builtins.lc 184:10-184:18 Type testdata/Builtins.lc 185:10-186:18 'Nat->Type testdata/Builtins.lc 185:10-186:18 Type testdata/Builtins.lc 185:10-185:18 Type testdata/Builtins.lc 186:10-186:18 'Nat->Type testdata/Builtins.lc 186:10-186:18 Type testdata/Builtins.lc 187:10-192:18 'Nat->Type testdata/Builtins.lc 187:10-192:18 Type testdata/Builtins.lc 187:10-189:18 Type testdata/Builtins.lc 187:10-189:18 'Nat->Type testdata/Builtins.lc 187:10-187:18 Type testdata/Builtins.lc 188:10-189:18 'Nat->Type testdata/Builtins.lc 188:10-189:18 Type testdata/Builtins.lc 188:10-188:18 Type testdata/Builtins.lc 189:10-189:18 'Nat->Type testdata/Builtins.lc 189:10-189:18 Type testdata/Builtins.lc 190:10-192:18 'Nat->Type testdata/Builtins.lc 190:10-192:18 Type testdata/Builtins.lc 190:10-190:18 Type testdata/Builtins.lc 191:10-192:18 'Nat->Type testdata/Builtins.lc 191:10-192:18 Type testdata/Builtins.lc 191:10-191:18 Type testdata/Builtins.lc 192:10-192:18 'Nat->Type testdata/Builtins.lc 192:10-192:18 Type testdata/Builtins.lc 184:30-184:39 Type testdata/Builtins.lc 178:7-178:15 Type->Type testdata/Builtins.lc 194:6-194:20 Type testdata/Builtins.lc 195:7-195:12 'BlendingFactor testdata/Builtins.lc 196:7-196:10 'BlendingFactor testdata/Builtins.lc 197:7-197:15 'BlendingFactor testdata/Builtins.lc 198:7-198:23 'BlendingFactor testdata/Builtins.lc 199:7-199:15 'BlendingFactor testdata/Builtins.lc 200:7-200:23 'BlendingFactor testdata/Builtins.lc 201:7-201:15 'BlendingFactor testdata/Builtins.lc 202:7-202:23 'BlendingFactor testdata/Builtins.lc 203:7-203:15 'BlendingFactor testdata/Builtins.lc 204:7-204:23 'BlendingFactor testdata/Builtins.lc 205:7-205:20 'BlendingFactor testdata/Builtins.lc 206:7-206:28 'BlendingFactor testdata/Builtins.lc 207:7-207:20 'BlendingFactor testdata/Builtins.lc 208:7-208:28 'BlendingFactor testdata/Builtins.lc 209:7-209:23 'BlendingFactor testdata/Builtins.lc 211:6-211:19 Type testdata/Builtins.lc 212:7-212:14 'BlendEquation testdata/Builtins.lc 213:7-213:19 'BlendEquation testdata/Builtins.lc 214:7-214:26 'BlendEquation testdata/Builtins.lc 215:7-215:10 'BlendEquation testdata/Builtins.lc 216:7-216:10 'BlendEquation testdata/Builtins.lc 218:6-218:20 Type testdata/Builtins.lc 219:7-219:12 'LogicOperation testdata/Builtins.lc 220:7-220:10 'LogicOperation testdata/Builtins.lc 221:7-221:17 'LogicOperation testdata/Builtins.lc 222:7-222:11 'LogicOperation testdata/Builtins.lc 223:7-223:18 'LogicOperation testdata/Builtins.lc 224:7-224:11 'LogicOperation testdata/Builtins.lc 225:7-225:10 'LogicOperation testdata/Builtins.lc 226:7-226:9 'LogicOperation testdata/Builtins.lc 227:7-227:10 'LogicOperation testdata/Builtins.lc 228:7-228:12 'LogicOperation testdata/Builtins.lc 229:7-229:13 'LogicOperation testdata/Builtins.lc 230:7-230:16 'LogicOperation testdata/Builtins.lc 231:7-231:19 'LogicOperation testdata/Builtins.lc 232:7-232:17 'LogicOperation testdata/Builtins.lc 233:7-233:11 'LogicOperation testdata/Builtins.lc 234:7-234:10 'LogicOperation testdata/Builtins.lc 236:6-236:22 Type testdata/Builtins.lc 237:7-237:13 'StencilOperation testdata/Builtins.lc 238:7-238:13 'StencilOperation testdata/Builtins.lc 239:7-239:16 'StencilOperation testdata/Builtins.lc 240:7-240:13 'StencilOperation testdata/Builtins.lc 241:7-241:17 'StencilOperation testdata/Builtins.lc 242:7-242:13 'StencilOperation testdata/Builtins.lc 243:7-243:17 'StencilOperation testdata/Builtins.lc 244:7-244:15 'StencilOperation testdata/Builtins.lc 246:6-246:24 Type testdata/Builtins.lc 247:7-247:12 'ComparisonFunction testdata/Builtins.lc 248:7-248:11 'ComparisonFunction testdata/Builtins.lc 249:7-249:12 'ComparisonFunction testdata/Builtins.lc 250:7-250:13 'ComparisonFunction testdata/Builtins.lc 251:7-251:14 'ComparisonFunction testdata/Builtins.lc 252:7-252:15 'ComparisonFunction testdata/Builtins.lc 253:7-253:13 'ComparisonFunction testdata/Builtins.lc 254:7-254:13 'ComparisonFunction testdata/Builtins.lc 256:6-256:21 Type testdata/Builtins.lc 257:7-257:17 'ProvokingVertex testdata/Builtins.lc 258:7-258:18 'ProvokingVertex testdata/Builtins.lc 260:6-260:14 Type testdata/Builtins.lc 261:7-261:16 'CullMode testdata/Builtins.lc 262:7-262:15 'CullMode testdata/Builtins.lc 263:7-263:15 'CullMode testdata/Builtins.lc 265:6-265:15 Type testdata/Builtins.lc 266:17-266:22 Type testdata/Builtins.lc 266:7-266:16 'Float->'PointSize testdata/Builtins.lc 267:7-267:23 'PointSize testdata/Builtins.lc 269:6-269:17 Type testdata/Builtins.lc 270:7-270:18 'PolygonMode testdata/Builtins.lc 271:20-271:29 Type testdata/Builtins.lc 271:7-271:19 'PointSize->'PolygonMode testdata/Builtins.lc 272:19-272:24 Type testdata/Builtins.lc 272:7-272:18 'Float->'PolygonMode testdata/Builtins.lc 274:6-274:19 Type testdata/Builtins.lc 275:7-275:15 'PolygonOffset testdata/Builtins.lc 276:14-276:19 Type testdata/Builtins.lc 274:6-276:25 Type testdata/Builtins.lc 276:20-276:25 Type testdata/Builtins.lc 276:7-276:13 'Float -> 'Float->'PolygonOffset testdata/Builtins.lc 278:6-278:28 Type testdata/Builtins.lc 279:7-279:16 'PointSpriteCoordOrigin testdata/Builtins.lc 280:7-280:16 'PointSpriteCoordOrigin testdata/Builtins.lc 283:6-283:11 Type->Type testdata/Builtins.lc 284:6-284:13 Type->Type testdata/Builtins.lc 285:6-285:11 Type->Type testdata/Builtins.lc 287:6-287:19 Type testdata/Builtins.lc 288:7-288:15 'PrimitiveType testdata/Builtins.lc 289:7-289:11 'PrimitiveType testdata/Builtins.lc 290:7-290:12 'PrimitiveType testdata/Builtins.lc 291:7-291:24 'PrimitiveType testdata/Builtins.lc 292:7-292:20 'PrimitiveType testdata/Builtins.lc 295:16-295:18 Type testdata/Builtins.lc 295:22-295:48 Type testdata/Builtins.lc 295:22-295:25 'Nat -> Type->Type testdata/Builtins.lc 295:28-295:33 Type testdata/Builtins.lc 295:37-295:48 Type testdata/Builtins.lc 295:37-295:40 'Nat -> Type->Type testdata/Builtins.lc 295:43-295:48 Type testdata/Builtins.lc 295:1-295:12 'Tuple0 -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 298:14-298:25 Type testdata/Builtins.lc 298:14-298:20 Type testdata/Builtins.lc 298:14-298:25 V2 testdata/Builtins.lc 298:1-298:8 {a} -> 'String->a testdata/Builtins.lc 299:14-299:25 Type testdata/Builtins.lc 299:14-299:20 Type testdata/Builtins.lc 299:14-299:25 V2 testdata/Builtins.lc 299:1-299:10 {a} -> 'String->a testdata/Builtins.lc 301:23-301:36 Type testdata/Builtins.lc 301:40-301:44 Type testdata/Builtins.lc 301:6-301:19 'PrimitiveType->Type testdata/Builtins.lc 302:26-302:34 Type testdata/Builtins.lc 302:38-302:111 Type testdata/Builtins.lc 302:38-302:49 Type testdata/Builtins.lc 302:53-302:111 Type testdata/Builtins.lc 302:53-302:66 Type testdata/Builtins.lc 302:70-302:111 Type testdata/Builtins.lc 302:70-302:85 Type testdata/Builtins.lc 302:89-302:111 Type testdata/Builtins.lc 302:89-302:102 'PrimitiveType->Type testdata/Builtins.lc 302:103-302:111 'PrimitiveType testdata/Builtins.lc 302:3-302:14 'CullMode -> 'PolygonMode -> 'PolygonOffset -> 'ProvokingVertex -> 'RasterContext Triangle testdata/Builtins.lc 303:26-303:35 Type testdata/Builtins.lc 303:39-303:108 Type testdata/Builtins.lc 303:39-303:44 Type testdata/Builtins.lc 303:48-303:108 Type testdata/Builtins.lc 303:48-303:70 Type testdata/Builtins.lc 303:89-303:108 Type testdata/Builtins.lc 303:89-303:102 'PrimitiveType->Type testdata/Builtins.lc 303:103-303:108 'PrimitiveType testdata/Builtins.lc 303:3-303:11 'PointSize -> 'Float -> 'PointSpriteCoordOrigin -> 'RasterContext Point testdata/Builtins.lc 304:26-304:31 Type testdata/Builtins.lc 304:35-304:107 Type testdata/Builtins.lc 304:35-304:50 Type testdata/Builtins.lc 304:89-304:107 Type testdata/Builtins.lc 304:89-304:102 'PrimitiveType->Type testdata/Builtins.lc 304:103-304:107 'PrimitiveType testdata/Builtins.lc 304:3-304:10 'Float -> 'ProvokingVertex -> 'RasterContext Line testdata/Builtins.lc 302:103-304:107 Type testdata/Builtins.lc 302:103-302:111 Type testdata/Builtins.lc 303:103-304:107 Type testdata/Builtins.lc 303:103-303:108 Type testdata/Builtins.lc 304:103-304:107 Type testdata/Builtins.lc 306:6-306:18 Type->Type testdata/Builtins.lc 308:27-308:56 Type testdata/Builtins.lc 308:27-308:35 Type->Type testdata/Builtins.lc 308:36-308:37 Type testdata/Builtins.lc 308:42-308:56 Type testdata/Builtins.lc 308:42-308:54 Type->Type testdata/Builtins.lc 308:55-308:56 Type testdata/Builtins.lc 307:3-307:9 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 307:11-307:24 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 309:42-309:56 Type testdata/Builtins.lc 309:42-309:54 Type->Type testdata/Builtins.lc 309:55-309:56 Type testdata/Builtins.lc 309:3-309:7 {a} -> 'Interpolated a testdata/Builtins.lc 313:14-314:32 Type->Type testdata/Builtins.lc 313:14-314:32 Type testdata/Builtins.lc 313:14-313:15 Type testdata/Builtins.lc 314:15-314:32 Type testdata/Builtins.lc 314:26-314:32 Type -> Type->Type testdata/Builtins.lc 314:26-314:32 Type->Type testdata/Builtins.lc 314:26-314:32 Type testdata/Builtins.lc 314:15-314:21 Type testdata/Builtins.lc 313:5-313:12 Type->Type testdata/Builtins.lc 317:27-320:82 Type->Type testdata/Builtins.lc 317:27-320:82 Type testdata/Builtins.lc 317:27-317:29 Type testdata/Builtins.lc 318:36-320:82 Type testdata/Builtins.lc 318:36-318:37 Type testdata/Builtins.lc 319:23-320:82 Type testdata/Builtins.lc 319:57-319:63 Type -> Type->Type testdata/Builtins.lc 319:57-319:63 Type->Type testdata/Builtins.lc 319:57-319:63 Type testdata/Builtins.lc 319:23-319:53 Type testdata/Builtins.lc 320:23-320:82 Type testdata/Builtins.lc 320:73-320:82 Type -> Type -> Type->Type testdata/Builtins.lc 320:73-320:82 Type -> Type->Type testdata/Builtins.lc 320:73-320:82 Type->Type testdata/Builtins.lc 320:73-320:82 Type testdata/Builtins.lc 320:23-320:69 Type testdata/Builtins.lc 317:5-317:21 Type->Type testdata/Builtins.lc 322:18-322:22 Type testdata/Builtins.lc 322:26-322:30 Type testdata/Builtins.lc 322:6-322:14 Type->Type testdata/Builtins.lc 323:60-323:70 Type testdata/Builtins.lc 323:60-323:68 Type->Type testdata/Builtins.lc 323:60-323:70 V1 testdata/Builtins.lc 323:3-323:13 {a} -> 'Blending a testdata/Builtins.lc 324:27-324:70 Type testdata/Builtins.lc 324:27-324:35 Type->Type testdata/Builtins.lc 324:27-324:70 V1 testdata/Builtins.lc 324:42-324:56 Type testdata/Builtins.lc 324:60-324:68 Type->Type testdata/Builtins.lc 324:3-324:15 {a} -> {b : 'Integral a} -> 'LogicOperation -> 'Blending a testdata/Builtins.lc 325:26-325:56 Type -> Type->Type testdata/Builtins.lc 325:27-325:40 Type testdata/Builtins.lc 325:42-325:55 Type testdata/Builtins.lc 326:29-327:74 Type testdata/Builtins.lc 326:29-326:97 Type -> Type->Type testdata/Builtins.lc 326:30-326:62 Type testdata/Builtins.lc 326:30-326:62 Type -> Type->Type testdata/Builtins.lc 326:31-326:45 Type testdata/Builtins.lc 326:47-326:61 Type testdata/Builtins.lc 326:64-326:96 Type testdata/Builtins.lc 326:64-326:96 Type -> Type->Type testdata/Builtins.lc 326:65-326:79 Type testdata/Builtins.lc 326:81-326:95 Type testdata/Builtins.lc 327:29-327:74 Type testdata/Builtins.lc 327:29-327:32 'Nat -> Type->Type testdata/Builtins.lc 327:35-327:40 Type testdata/Builtins.lc 327:60-327:74 Type testdata/Builtins.lc 327:60-327:68 Type->Type testdata/Builtins.lc 327:69-327:74 Type testdata/Builtins.lc 325:3-325:8 'Tuple2 'BlendEquation 'BlendEquation -> 'Tuple2 ('Tuple2 'BlendingFactor 'BlendingFactor) ('Tuple2 'BlendingFactor 'BlendingFactor) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Blending 'Float testdata/Builtins.lc 323:60-327:74 Type testdata/Builtins.lc 324:27-327:74 Type testdata/Builtins.lc 334:6-334:18 Type testdata/Builtins.lc 335:6-335:16 Type testdata/Builtins.lc 336:6-336:11 Type testdata/Builtins.lc 338:27-338:31 Type testdata/Builtins.lc 338:35-338:39 Type testdata/Builtins.lc 338:6-338:23 Type->Type testdata/Builtins.lc 339:27-340:101 Type testdata/Builtins.lc 339:27-340:101 V7 testdata/Builtins.lc 339:34-339:43 'Nat -> Type->Type testdata/Builtins.lc 339:27-340:101 'Nat testdata/Builtins.lc 339:27-340:101 V5 testdata/Builtins.lc 339:46-339:50 Type testdata/Builtins.lc 339:27-340:101 V4 testdata/Builtins.lc 339:60-339:69 'Nat -> Type->Type testdata/Builtins.lc 339:27-340:101 V2 testdata/Builtins.lc 339:75-339:78 Type->Type testdata/Builtins.lc 339:85-339:93 Type->Type testdata/Builtins.lc 340:71-340:88 Type->Type testdata/Builtins.lc 340:90-340:95 Type->Type testdata/Builtins.lc 339:3-339: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 341:26-341:44 Type testdata/Builtins.lc 341:48-341:101 Type testdata/Builtins.lc 341:48-341:52 Type testdata/Builtins.lc 341:71-341:101 Type testdata/Builtins.lc 341:71-341:88 Type->Type testdata/Builtins.lc 341:90-341:101 Type testdata/Builtins.lc 341:90-341:95 Type->Type testdata/Builtins.lc 341:96-341:101 Type testdata/Builtins.lc 341:3-341:10 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 342:26-342:38 Type testdata/Builtins.lc 342:42-342:103 Type testdata/Builtins.lc 342:42-342:52 Type testdata/Builtins.lc 342:56-342:103 Type testdata/Builtins.lc 342:56-342:66 Type testdata/Builtins.lc 342:71-342:103 Type testdata/Builtins.lc 342:71-342:88 Type->Type testdata/Builtins.lc 342:90-342:103 Type testdata/Builtins.lc 342:90-342:97 Type->Type testdata/Builtins.lc 342:98-342:103 Type testdata/Builtins.lc 342:3-342:12 'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation ('Stencil 'Int32) testdata/Builtins.lc 339:27-342:103 Type testdata/Builtins.lc 341:90-342:103 Type testdata/Builtins.lc 345:32-349:146 Type->Type testdata/Builtins.lc 345:32-349:146 Type testdata/Builtins.lc 345:32-345:33 Type testdata/Builtins.lc 346:14-349:146 Type testdata/Builtins.lc 346:60-346:68 Type -> Type->Type testdata/Builtins.lc 346:60-346:68 Type->Type testdata/Builtins.lc 346:60-346:68 Type testdata/Builtins.lc 346:14-346:56 Type testdata/Builtins.lc 347:14-349:146 Type testdata/Builtins.lc 347:82-347:94 Type -> Type -> Type->Type testdata/Builtins.lc 347:82-347:94 Type -> Type->Type testdata/Builtins.lc 347:82-347:94 Type->Type testdata/Builtins.lc 347:82-347:94 Type testdata/Builtins.lc 347:14-347:78 Type testdata/Builtins.lc 348:14-349:146 Type testdata/Builtins.lc 348:104-348:120 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 348:104-348:120 Type -> Type -> Type->Type testdata/Builtins.lc 348:104-348:120 Type -> Type->Type testdata/Builtins.lc 348:104-348:120 Type->Type testdata/Builtins.lc 348:104-348:120 Type testdata/Builtins.lc 348:14-348:100 Type testdata/Builtins.lc 349:14-349:146 Type testdata/Builtins.lc 349:126-349:146 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 349:126-349:146 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 349:126-349:146 Type -> Type -> Type->Type testdata/Builtins.lc 349:126-349:146 Type -> Type->Type testdata/Builtins.lc 349:126-349:146 Type->Type testdata/Builtins.lc 349:126-349:146 Type testdata/Builtins.lc 349:14-349:122 Type testdata/Builtins.lc 345:5-345:12 Type->Type testdata/Builtins.lc 352:15-356:36 Type->Type testdata/Builtins.lc 352:15-356:36 Type testdata/Builtins.lc 352:25-352:69 Type -> Type->Type testdata/Builtins.lc 352:25-352:69 Type->Type testdata/Builtins.lc 352:25-352:69 Type testdata/Builtins.lc 352:26-352:43 Type testdata/Builtins.lc 352:26-352:43 Type->Type testdata/Builtins.lc 352:48-352:65 Type testdata/Builtins.lc 352:48-352:65 Type->Type testdata/Builtins.lc 352:15-352:21 Type testdata/Builtins.lc 353:15-356:36 Type testdata/Builtins.lc 353:29-353:95 Type -> Type -> Type->Type testdata/Builtins.lc 353:29-353:95 Type -> Type->Type testdata/Builtins.lc 353:29-353:95 Type->Type testdata/Builtins.lc 353:29-353:95 Type testdata/Builtins.lc 353:30-353:47 Type testdata/Builtins.lc 353:30-353:47 Type->Type testdata/Builtins.lc 353:52-353:69 Type testdata/Builtins.lc 353:52-353:69 Type->Type testdata/Builtins.lc 353:74-353:91 Type testdata/Builtins.lc 353:74-353:91 Type->Type testdata/Builtins.lc 353:15-353:25 Type testdata/Builtins.lc 354:15-356:36 Type testdata/Builtins.lc 354:34-354:122 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 354:34-354:122 Type -> Type -> Type->Type testdata/Builtins.lc 354:34-354:122 Type -> Type->Type testdata/Builtins.lc 354:34-354:122 Type->Type testdata/Builtins.lc 354:34-354:122 Type testdata/Builtins.lc 354:35-354:52 Type testdata/Builtins.lc 354:35-354:52 Type->Type testdata/Builtins.lc 354:57-354:74 Type testdata/Builtins.lc 354:57-354:74 Type->Type testdata/Builtins.lc 354:79-354:96 Type testdata/Builtins.lc 354:79-354:96 Type->Type testdata/Builtins.lc 354:101-354:118 Type testdata/Builtins.lc 354:101-354:118 Type->Type testdata/Builtins.lc 354:15-354:29 Type testdata/Builtins.lc 355:15-356:36 Type testdata/Builtins.lc 355:38-355:148 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 355:38-355:148 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 355:38-355:148 Type -> Type -> Type->Type testdata/Builtins.lc 355:38-355:148 Type -> Type->Type testdata/Builtins.lc 355:38-355:148 Type->Type testdata/Builtins.lc 355:38-355:148 Type testdata/Builtins.lc 355:39-355:56 Type testdata/Builtins.lc 355:39-355:56 Type->Type testdata/Builtins.lc 355:61-355:78 Type testdata/Builtins.lc 355:61-355:78 Type->Type testdata/Builtins.lc 355:83-355:100 Type testdata/Builtins.lc 355:83-355:100 Type->Type testdata/Builtins.lc 355:105-355:122 Type testdata/Builtins.lc 355:105-355:122 Type->Type testdata/Builtins.lc 355:127-355:144 Type testdata/Builtins.lc 355:127-355:144 Type->Type testdata/Builtins.lc 355:15-355:33 Type testdata/Builtins.lc 356:19-356:36 Type testdata/Builtins.lc 356:19-356:36 Type->Type testdata/Builtins.lc 352:5-352:13 Type->Type testdata/Builtins.lc 358:6-358:12 Type->Type testdata/Builtins.lc 360:15-360:46 Type testdata/Builtins.lc 360:15-360:46 V3 testdata/Builtins.lc 360:15-360:46 V2 testdata/Builtins.lc 360:26-360:32 Type->Type testdata/Builtins.lc 360:38-360:44 Type->Type testdata/Builtins.lc 360:1-360:10 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 361:18-361:52 Type testdata/Builtins.lc 361:18-361:52 V1 testdata/Builtins.lc 361:23-361:27 Type testdata/Builtins.lc 361:32-361:38 Type->Type testdata/Builtins.lc 361:44-361:50 Type->Type testdata/Builtins.lc 361:1-361:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 363:22-363:35 Type testdata/Builtins.lc 363:6-363:15 'PrimitiveType -> Type->Type testdata/Builtins.lc 365:18-365:59 Type testdata/Builtins.lc 365:18-365:59 V5 testdata/Builtins.lc 365:18-365:59 V4 testdata/Builtins.lc 365:29-365:38 'PrimitiveType -> Type->Type testdata/Builtins.lc 365:18-365:59 'PrimitiveType testdata/Builtins.lc 365:18-365:59 V2 testdata/Builtins.lc 365:46-365:55 'PrimitiveType -> Type->Type testdata/Builtins.lc 365:1-365:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 367:39-367:96 Type testdata/Builtins.lc 367:39-367:53 {a} -> a->Type testdata/Builtins.lc 367:54-367:55 V0 testdata/Builtins.lc 367:54-367:55 V2 testdata/Builtins.lc 367:60-367:96 Type testdata/Builtins.lc 367:60-367:66 Type testdata/Builtins.lc 367:70-367:96 Type testdata/Builtins.lc 367:70-367:71 V3 testdata/Builtins.lc 367:75-367:96 Type testdata/Builtins.lc 367:75-367:81 Type->Type testdata/Builtins.lc 367:83-367:96 Type testdata/Builtins.lc 367:83-367:92 'PrimitiveType -> Type->Type testdata/Builtins.lc 367:93-367:94 'PrimitiveType testdata/Builtins.lc 367:93-367:94 V5 testdata/Builtins.lc 367:95-367:96 Type testdata/Builtins.lc 367:1-367:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 368:42-368:106 Type testdata/Builtins.lc 368:42-368:56 {a} -> a->Type testdata/Builtins.lc 368:57-368:58 V0 testdata/Builtins.lc 368:57-368:58 V4 testdata/Builtins.lc 368:60-368:106 Type testdata/Builtins.lc 368:60-368:61 Type testdata/Builtins.lc 368:60-368:61 V4 testdata/Builtins.lc 368:64-368:74 Type testdata/Builtins.lc 368:64-368:71 Type->Type testdata/Builtins.lc 368:72-368:74 Type testdata/Builtins.lc 368:72-368:74 V2 testdata/Builtins.lc 368:79-368:106 Type testdata/Builtins.lc 368:79-368:81 Type testdata/Builtins.lc 368:85-368:106 Type testdata/Builtins.lc 368:85-368:91 Type->Type testdata/Builtins.lc 368:93-368:106 Type testdata/Builtins.lc 368:93-368:102 'PrimitiveType -> Type->Type testdata/Builtins.lc 368:103-368:104 'PrimitiveType testdata/Builtins.lc 368:103-368:104 V6 testdata/Builtins.lc 368:105-368:106 Type testdata/Builtins.lc 368:1-368:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 370:19-370:79 Type testdata/Builtins.lc 370:19-370:79 V5 testdata/Builtins.lc 370:19-370:79 V4 testdata/Builtins.lc 370:31-370:37 Type->Type testdata/Builtins.lc 370:39-370:48 'PrimitiveType -> Type->Type testdata/Builtins.lc 370:19-370:79 'PrimitiveType testdata/Builtins.lc 370:19-370:79 V2 testdata/Builtins.lc 370:58-370:64 Type->Type testdata/Builtins.lc 370:66-370:75 'PrimitiveType -> Type->Type testdata/Builtins.lc 371:19-371:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 371:19-371:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) testdata/Builtins.lc 371:19-371:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) testdata/Builtins.lc 371:19-371:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 371:19-371:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 371:19-371:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 371:30-371:42 V1->V1 testdata/Builtins.lc 371:30-371:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 371:1-371:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 373:15-373:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 373:1-373:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) testdata/Builtins.lc 374:19-374:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 374:1-374:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) testdata/Builtins.lc 376:6-376:18 Type testdata/Builtins.lc 376:21-376:28 'DepthHandler testdata/Builtins.lc 376:31-376:43 'DepthHandler testdata/Builtins.lc 393:23-403:82 Type->Type testdata/Builtins.lc 393:23-403:82 Type testdata/Builtins.lc 393:23-393:25 Type testdata/Builtins.lc 394:25-403:82 Type testdata/Builtins.lc 394:25-394:26 Type testdata/Builtins.lc 395:19-403:82 Type testdata/Builtins.lc 395:39-395:45 Type -> Type->Type testdata/Builtins.lc 395:39-395:45 Type->Type testdata/Builtins.lc 395:39-395:45 Type testdata/Builtins.lc 395:19-395:35 Type testdata/Builtins.lc 396:19-403:82 Type testdata/Builtins.lc 396:48-401:58 Type -> Type -> Type->Type testdata/Builtins.lc 396:48-401:58 Type -> Type->Type testdata/Builtins.lc 396:48-401:58 Type->Type testdata/Builtins.lc 396:48-401:58 Type testdata/Builtins.lc 396:48-396:57 Type->Type testdata/Builtins.lc 396:48-396:57 Type testdata/Builtins.lc 396:48-396:57 Type -> Type -> Type->Type testdata/Builtins.lc 401:52-401:58 Type testdata/Builtins.lc 401:52-401:58 Type->Type testdata/Builtins.lc 401:52-401:58 Type -> Type->Type testdata/Builtins.lc 396:19-396:44 Type testdata/Builtins.lc 397:19-403:82 Type testdata/Builtins.lc 397:57-402:70 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 397:57-402:70 Type -> Type -> Type->Type testdata/Builtins.lc 397:57-402:70 Type -> Type->Type testdata/Builtins.lc 397:57-402:70 Type->Type testdata/Builtins.lc 397:57-402:70 Type testdata/Builtins.lc 397:57-397:69 Type->Type testdata/Builtins.lc 397:57-397:69 Type testdata/Builtins.lc 397:57-397:69 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 402:61-402:70 Type testdata/Builtins.lc 402:61-402:70 Type->Type testdata/Builtins.lc 402:61-402:70 Type -> Type -> Type->Type testdata/Builtins.lc 397:19-397:53 Type testdata/Builtins.lc 398:19-403:82 Type testdata/Builtins.lc 398:66-403:82 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 398:66-403:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 398:66-403:82 Type -> Type -> Type->Type testdata/Builtins.lc 398:66-403:82 Type -> Type->Type testdata/Builtins.lc 398:66-403:82 Type->Type testdata/Builtins.lc 398:66-403:82 Type testdata/Builtins.lc 398:66-398:81 Type->Type testdata/Builtins.lc 398:66-398:81 Type testdata/Builtins.lc 398:66-398:81 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 403:70-403:82 Type testdata/Builtins.lc 403:70-403:82 Type->Type testdata/Builtins.lc 403:70-403:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 398:19-398:62 Type testdata/Builtins.lc 399:25-399:36 Type testdata/Builtins.lc 399:34-399:36 Type->Type testdata/Builtins.lc 399:34-399:36 Type testdata/Builtins.lc 399:25-399:30 Type testdata/Builtins.lc 393:5-393:17 Type->Type testdata/Builtins.lc 407:18-407:21 Type testdata/Builtins.lc 407:25-407:53 Type testdata/Builtins.lc 407:25-407:37 Type testdata/Builtins.lc 407:41-407:53 Type testdata/Builtins.lc 407:41-407:45 Type testdata/Builtins.lc 407:49-407:53 Type testdata/Builtins.lc 407:6-407:14 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 409:20-409:78 Type testdata/Builtins.lc 409:20-409:78 V3 testdata/Builtins.lc 409:25-409:30 Type testdata/Builtins.lc 409:35-409:43 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 409:20-409:78 'Nat testdata/Builtins.lc 409:20-409:78 V2 testdata/Builtins.lc 409:53-409:61 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 409:64-409:76 'DepthHandler testdata/Builtins.lc 409:1-409:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 411:21-411:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 411:32-411:46 V1->V1 testdata/Builtins.lc 411:32-411:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 411:1-411:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) testdata/Builtins.lc 418:21-422:62 Type testdata/Builtins.lc 418:21-422:62 V7 testdata/Builtins.lc 418:25-418:41 Type->Type testdata/Builtins.lc 418:21-422:62 V5 testdata/Builtins.lc 418:21-422:62 V4 testdata/Builtins.lc 418:49-418:62 Type -> Type->Type testdata/Builtins.lc 418:64-418:75 Type testdata/Builtins.lc 418:64-418:67 'Nat -> Type->Type testdata/Builtins.lc 418:70-418:75 Type testdata/Builtins.lc 419:26-419:31 Type testdata/Builtins.lc 421:20-421:33 'PrimitiveType->Type testdata/Builtins.lc 418:21-422:62 'PrimitiveType testdata/Builtins.lc 422:20-422:29 'PrimitiveType -> Type->Type testdata/Builtins.lc 422:37-422:45 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 422:48-422:60 'DepthHandler testdata/Builtins.lc 418:1-418: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 424:20-424:56 Type testdata/Builtins.lc 424:20-424:56 V3 testdata/Builtins.lc 424:25-424:29 Type testdata/Builtins.lc 424:34-424:42 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 424:20-424:56 'Nat testdata/Builtins.lc 424:20-424:56 V2 testdata/Builtins.lc 424:52-424:56 Type testdata/Builtins.lc 424:1-424:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 426:21-426:84 Type testdata/Builtins.lc 426:21-426:84 V5 testdata/Builtins.lc 426:26-426:30 Type testdata/Builtins.lc 426:35-426:41 Type->Type testdata/Builtins.lc 426:43-426:51 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 426:21-426:84 'Nat testdata/Builtins.lc 426:21-426:84 V4 testdata/Builtins.lc 426:21-426:84 'DepthHandler testdata/Builtins.lc 426:21-426:84 V2 testdata/Builtins.lc 426:62-426:68 Type->Type testdata/Builtins.lc 426:70-426:78 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 427:21-427:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 427:21-427:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) testdata/Builtins.lc 427:21-427:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) testdata/Builtins.lc 427:21-427:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 427:21-427:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 427:21-427:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 427:35-427:49 V0->'Bool testdata/Builtins.lc 427:35-427:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 427:1-427:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 429:17-429:60 Type testdata/Builtins.lc 429:17-429:60 V7 testdata/Builtins.lc 429:17-429:60 V6 testdata/Builtins.lc 429:28-429:36 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 429:17-429:60 'Nat testdata/Builtins.lc 429:17-429:60 V4 testdata/Builtins.lc 429:17-429:60 'DepthHandler testdata/Builtins.lc 429:17-429:60 V2 testdata/Builtins.lc 429:46-429:54 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 429:1-429:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 431:18-431:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 431:29-431:40 V1->V1 testdata/Builtins.lc 431:29-431:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 431:1-431:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 436:13-436:26 Type->Type testdata/Builtins.lc 441:13-441:28 Type->Type testdata/Builtins.lc 444:10-445:36 V0->Type testdata/Builtins.lc 444:10-445:36 Type testdata/Builtins.lc 444:10-444:23 Type->Type testdata/Builtins.lc 444:10-444:23 Type testdata/Builtins.lc 444:10-444:23 Type -> 'Nat->Type testdata/Builtins.lc 444:10-444:23 'Nat->Type testdata/Builtins.lc 444:37-444:44 Type testdata/Builtins.lc 444:37-444:44 V1 testdata/Builtins.lc 445:10-445:36 Type testdata/Builtins.lc 445:10-445:23 Type->Type testdata/Builtins.lc 445:10-445:23 Type testdata/Builtins.lc 445:31-445:36 Type testdata/Builtins.lc 443:7-443:20 Type->Type testdata/Builtins.lc 443:7-443:65 Type testdata/Builtins.lc 443:46-443:65 Type testdata/Builtins.lc 443:46-443:63 Type->Type testdata/Builtins.lc 443:64-443:65 Type testdata/Builtins.lc 444:37-445:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a testdata/Builtins.lc 444:37-445:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 testdata/Builtins.lc 444:69-444:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) testdata/Builtins.lc 444:69-444:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) testdata/Builtins.lc 444:69-444:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) testdata/Builtins.lc 444:69-444:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) testdata/Builtins.lc 444:69-444:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) testdata/Builtins.lc 444:69-444:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) testdata/Builtins.lc 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) testdata/Builtins.lc 444:69-444: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 444:69-444:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) testdata/Builtins.lc 444:69-444:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) testdata/Builtins.lc 444:69-444: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 444:77-444:87 'Blending V1 testdata/Builtins.lc 444:77-444:87 {a} -> 'Blending a testdata/Builtins.lc 444:89-444:111 'VecScalar V2 'Bool testdata/Builtins.lc 444:89-444:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 444:92-444:96 V0 testdata/Builtins.lc 444:92-444:96 'Bool testdata/Builtins.lc 444:97-444:101 'Bool testdata/Builtins.lc 444:102-444:106 'Bool testdata/Builtins.lc 444:107-444:111 'Bool testdata/Builtins.lc 445:31-445:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 testdata/Builtins.lc 445:60-445:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) testdata/Builtins.lc 445:60-445:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) testdata/Builtins.lc 445:60-445:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 445:60-445:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 445:68-445:72 'ComparisonFunction testdata/Builtins.lc 445:73-445:77 'Bool testdata/Builtins.lc 443:29-443:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b testdata/Builtins.lc 452:24-452:27 Type testdata/Builtins.lc 452:6-452:17 'Nat -> Type->Type testdata/Builtins.lc 453:19-453:109 Type testdata/Builtins.lc 453:19-453:27 Type->Type testdata/Builtins.lc 453:28-453:29 Type testdata/Builtins.lc 453:33-453:39 Type->Type testdata/Builtins.lc 453:41-453:49 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 453:50-453:51 'Nat testdata/Builtins.lc 453:19-453:109 'DepthHandler testdata/Builtins.lc 453:19-453:109 V2 testdata/Builtins.lc 453:55-453:69 Type testdata/Builtins.lc 453:55-453:67 Type->Type testdata/Builtins.lc 453:68-453:69 Type testdata/Builtins.lc 453:75-453:109 Type testdata/Builtins.lc 453:75-453:86 'Nat -> Type->Type testdata/Builtins.lc 453:87-453:88 'Nat testdata/Builtins.lc 453:89-453:90 Type testdata/Builtins.lc 453:94-453:109 Type testdata/Builtins.lc 453:94-453:105 'Nat -> Type->Type testdata/Builtins.lc 453:106-453:107 'Nat testdata/Builtins.lc 453:108-453:109 Type testdata/Builtins.lc 453:3-453:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 454:20-454:117 Type testdata/Builtins.lc 454:20-454:36 {a} -> a->Type testdata/Builtins.lc 454:37-454:38 V0 testdata/Builtins.lc 454:37-454:38 Type testdata/Builtins.lc 454:40-454:55 Type->Type testdata/Builtins.lc 454:20-454:117 V2 testdata/Builtins.lc 454:59-454:74 Type testdata/Builtins.lc 454:59-454:70 'Nat -> Type->Type testdata/Builtins.lc 454:71-454:72 'Nat testdata/Builtins.lc 454:73-454:74 Type testdata/Builtins.lc 454:77-454:90 Type->Type testdata/Builtins.lc 454:102-454:117 Type testdata/Builtins.lc 454:102-454:113 'Nat -> Type->Type testdata/Builtins.lc 454:114-454:115 'Nat testdata/Builtins.lc 454:116-454:117 Type testdata/Builtins.lc 454:3-454:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 456:34-456:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 456:50-456:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) testdata/Builtins.lc 456:50-456:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 456:1-456: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 458:1-458:20 {a} -> a->a testdata/Builtins.lc 460:15-460:18 Type testdata/Builtins.lc 460:22-460:34 Type testdata/Builtins.lc 460:22-460:26 Type testdata/Builtins.lc 460:30-460:34 Type testdata/Builtins.lc 460:6-460:11 'Nat -> Type->Type testdata/Builtins.lc 461:48-462:56 Type testdata/Builtins.lc 461:48-461:51 Type->Type testdata/Builtins.lc 461:52-461:53 Type testdata/Builtins.lc 461:52-461:53 V3 testdata/Builtins.lc 461:55-462:56 Type testdata/Builtins.lc 461:55-461:60 Type testdata/Builtins.lc 461:55-461:60 V2 testdata/Builtins.lc 461:63-461:76 Type testdata/Builtins.lc 461:63-461:72 'Nat -> Type->Type testdata/Builtins.lc 461:73-461:74 'Nat testdata/Builtins.lc 461:73-461:74 V4 testdata/Builtins.lc 461:75-461:76 Type testdata/Builtins.lc 462:26-462:56 Type testdata/Builtins.lc 462:26-462:31 Type testdata/Builtins.lc 462:36-462:56 Type testdata/Builtins.lc 462:36-462:41 'Nat -> Type->Type testdata/Builtins.lc 462:42-462:43 'Nat testdata/Builtins.lc 462:42-462:43 V7 testdata/Builtins.lc 462:45-462:56 Type testdata/Builtins.lc 462:45-462:50 Type->Type testdata/Builtins.lc 462:51-462:56 Type testdata/Builtins.lc 461:3-461:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 463:37-463:67 Type testdata/Builtins.lc 463:37-463:42 Type testdata/Builtins.lc 463:47-463:67 Type testdata/Builtins.lc 463:47-463:52 'Nat -> Type->Type testdata/Builtins.lc 463:53-463:54 'Nat testdata/Builtins.lc 463:53-463:54 V2 testdata/Builtins.lc 463:56-463:67 Type testdata/Builtins.lc 463:56-463:61 Type->Type testdata/Builtins.lc 463:62-463:67 Type testdata/Builtins.lc 463:3-463:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 464:37-464:67 Type testdata/Builtins.lc 464:37-464:40 Type testdata/Builtins.lc 464:47-464:67 Type testdata/Builtins.lc 464:47-464:52 'Nat -> Type->Type testdata/Builtins.lc 464:53-464:54 'Nat testdata/Builtins.lc 464:53-464:54 V2 testdata/Builtins.lc 464:56-464:67 Type testdata/Builtins.lc 464:56-464:63 Type->Type testdata/Builtins.lc 464:64-464:67 Type testdata/Builtins.lc 464:3-464:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) testdata/Builtins.lc 467:26-467:54 Type testdata/Builtins.lc 467:26-467:37 'Nat -> Type->Type testdata/Builtins.lc 467:26-467:54 V1 testdata/Builtins.lc 467:45-467:50 'Nat -> Type->Type testdata/Builtins.lc 467:3-467:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a testdata/Builtins.lc 468:26-468:37 'Nat -> Type->Type testdata/Builtins.lc 468:40-468:74 Type testdata/Builtins.lc 468:40-468:74 Type -> Type->Type testdata/Builtins.lc 468:41-468:52 Type testdata/Builtins.lc 468:41-468:46 Type->Type testdata/Builtins.lc 468:47-468:52 Type testdata/Builtins.lc 468:54-468:72 Type testdata/Builtins.lc 468:54-468:59 Type->Type testdata/Builtins.lc 468:61-468:72 Type testdata/Builtins.lc 468:61-468:64 'Nat -> Type->Type testdata/Builtins.lc 468:67-468:72 Type testdata/Builtins.lc 468:78-468:105 Type testdata/Builtins.lc 468:78-468:83 'Nat -> Type->Type testdata/Builtins.lc 468:87-468:105 Type testdata/Builtins.lc 468:87-468:92 Type->Type testdata/Builtins.lc 468:94-468:105 Type testdata/Builtins.lc 468:94-468:97 'Nat -> Type->Type testdata/Builtins.lc 468:100-468:105 Type testdata/Builtins.lc 468:3-468: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 462:42-468:105 Type testdata/Builtins.lc 462:42-462:56 Type testdata/Builtins.lc 463:53-468:105 Type testdata/Builtins.lc 463:53-463:67 Type testdata/Builtins.lc 464:53-468:105 Type testdata/Builtins.lc 464:53-464:67 Type testdata/Builtins.lc 467:26-468:105 Type testdata/Builtins.lc 470:6-470:12 Type testdata/Builtins.lc 471:26-471:51 Type testdata/Builtins.lc 471:26-471:37 'Nat -> Type->Type testdata/Builtins.lc 471:26-471:51 'Nat testdata/Builtins.lc 471:26-471:51 V3 testdata/Builtins.lc 471:26-471:51 V1 testdata/Builtins.lc 471:45-471:51 Type testdata/Builtins.lc 471:3-471:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 477:34-477:73 Type testdata/Builtins.lc 477:34-477:37 Type->Type testdata/Builtins.lc 477:39-477:55 Type->Type testdata/Builtins.lc 477:34-477:73 V1 testdata/Builtins.lc 477:1-477:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 477:10-477:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 477:19-477:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 478:35-478:80 Type testdata/Builtins.lc 478:35-478:80 V3 testdata/Builtins.lc 478:39-478:55 Type->Type testdata/Builtins.lc 478:35-478:80 V1 testdata/Builtins.lc 478:59-478:62 Type->Type testdata/Builtins.lc 478:1-478:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 478:11-478:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 478:21-478:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 479:35-479:75 Type testdata/Builtins.lc 479:35-479:38 Type->Type testdata/Builtins.lc 479:35-479:75 V5 testdata/Builtins.lc 479:35-479:75 V4 testdata/Builtins.lc 479:46-479:55 'Nat -> Type->Type testdata/Builtins.lc 479:35-479:75 'Nat testdata/Builtins.lc 479:35-479:75 V2 testdata/Builtins.lc 479:1-479:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 479:10-479:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 480:35-480:75 Type testdata/Builtins.lc 480:35-480:38 Type->Type testdata/Builtins.lc 480:35-480:75 V5 testdata/Builtins.lc 480:35-480:75 V4 testdata/Builtins.lc 480:46-480:55 'Nat -> Type->Type testdata/Builtins.lc 480:35-480:75 'Nat testdata/Builtins.lc 480:35-480:75 V2 testdata/Builtins.lc 480:1-480:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 480:11-480:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 481:34-481:71 Type testdata/Builtins.lc 481:34-481:40 Type->Type testdata/Builtins.lc 481:42-481:58 Type->Type testdata/Builtins.lc 481:34-481:71 V1 testdata/Builtins.lc 481:1-481:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a testdata/Builtins.lc 483:35-483:80 Type testdata/Builtins.lc 483:35-483:43 Type->Type testdata/Builtins.lc 483:35-483:80 V5 testdata/Builtins.lc 483:35-483:80 V4 testdata/Builtins.lc 483:51-483:60 'Nat -> Type->Type testdata/Builtins.lc 483:35-483:80 'Nat testdata/Builtins.lc 483:35-483:80 V2 testdata/Builtins.lc 483:1-483:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 483:11-483:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 483:20-483:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 484:35-484:80 Type testdata/Builtins.lc 484:35-484:43 Type->Type testdata/Builtins.lc 484:35-484:80 V5 testdata/Builtins.lc 484:35-484:80 V4 testdata/Builtins.lc 484:51-484:60 'Nat -> Type->Type testdata/Builtins.lc 484:35-484:80 'Nat testdata/Builtins.lc 484:35-484:80 V2 testdata/Builtins.lc 484:1-484:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 484:12-484:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 484:22-484:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 485:35-485:75 Type testdata/Builtins.lc 485:35-485:43 Type->Type testdata/Builtins.lc 485:35-485:75 V5 testdata/Builtins.lc 485:35-485:75 V4 testdata/Builtins.lc 485:51-485:60 'Nat -> Type->Type testdata/Builtins.lc 485:35-485:75 'Nat testdata/Builtins.lc 485:35-485:75 V2 testdata/Builtins.lc 485:1-485:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 486:35-486:102 Type testdata/Builtins.lc 486:35-486:43 Type->Type testdata/Builtins.lc 486:35-486:102 V7 testdata/Builtins.lc 486:35-486:102 V6 testdata/Builtins.lc 486:51-486:60 'Nat -> Type->Type testdata/Builtins.lc 486:35-486:102 'Nat testdata/Builtins.lc 486:35-486:102 V4 testdata/Builtins.lc 486:35-486:102 V3 testdata/Builtins.lc 486:70-486:79 'Nat -> Type->Type testdata/Builtins.lc 486:82-486:86 Type testdata/Builtins.lc 486:1-486: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 486:14-486: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 487:35-487:83 Type testdata/Builtins.lc 487:35-487:43 Type->Type testdata/Builtins.lc 487:35-487:83 V5 testdata/Builtins.lc 487:35-487:83 V4 testdata/Builtins.lc 487:51-487:60 'Nat -> Type->Type testdata/Builtins.lc 487:35-487:83 'Nat testdata/Builtins.lc 487:35-487:83 V2 testdata/Builtins.lc 487:74-487:78 Type testdata/Builtins.lc 487:1-487:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 487:15-487:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 489:34-489:38 Type testdata/Builtins.lc 489:42-489:54 Type testdata/Builtins.lc 489:42-489:46 Type testdata/Builtins.lc 489:50-489:54 Type testdata/Builtins.lc 489:1-489:8 'Bool -> 'Bool->'Bool testdata/Builtins.lc 489:10-489:16 'Bool -> 'Bool->'Bool testdata/Builtins.lc 489:18-489:25 'Bool -> 'Bool->'Bool testdata/Builtins.lc 490:35-490:66 Type testdata/Builtins.lc 490:35-490:66 V3 testdata/Builtins.lc 490:39-490:48 'Nat -> Type->Type testdata/Builtins.lc 490:35-490:66 'Nat testdata/Builtins.lc 490:35-490:66 V1 testdata/Builtins.lc 490:51-490:55 Type testdata/Builtins.lc 490:1-490:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a testdata/Builtins.lc 491:34-491:58 Type testdata/Builtins.lc 491:34-491:43 'Nat -> Type->Type testdata/Builtins.lc 491:34-491:58 'Nat testdata/Builtins.lc 491:34-491:58 V1 testdata/Builtins.lc 491:46-491:50 Type testdata/Builtins.lc 491:54-491:58 Type testdata/Builtins.lc 491:1-491:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 491:10-491:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 495:35-495:67 Type testdata/Builtins.lc 495:35-495:67 V3 testdata/Builtins.lc 495:39-495:48 'Nat -> Type->Type testdata/Builtins.lc 495:35-495:67 'Nat testdata/Builtins.lc 495:35-495:67 V1 testdata/Builtins.lc 495:51-495:56 Type testdata/Builtins.lc 494:1-494:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:11-494:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:22-494:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:32-494:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:43-494:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:53-494:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:64-494:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:73-494:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:83-494:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:96-494:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:109-494:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:118-494:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:128-494:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:137-494:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:147-494:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:156-494:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:165-494:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:175-494:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:185-494:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:195-494:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 496:35-496:72 Type testdata/Builtins.lc 496:35-496:72 V3 testdata/Builtins.lc 496:39-496:48 'Nat -> Type->Type testdata/Builtins.lc 496:35-496:72 'Nat testdata/Builtins.lc 496:35-496:72 V1 testdata/Builtins.lc 496:51-496:56 Type testdata/Builtins.lc 496:1-496:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 496:10-496:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 499:35-499:67 Type testdata/Builtins.lc 499:35-499:67 V3 testdata/Builtins.lc 499:39-499:48 'Nat -> Type->Type testdata/Builtins.lc 499:35-499:67 'Nat testdata/Builtins.lc 499:35-499:67 V1 testdata/Builtins.lc 499:51-499:56 Type testdata/Builtins.lc 498:1-498:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 498:12-498:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 498:23-498:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 498:34-498:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 498:49-498:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 498:59-498:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 500:35-500:75 Type testdata/Builtins.lc 500:35-500:38 Type->Type testdata/Builtins.lc 500:35-500:75 V5 testdata/Builtins.lc 500:35-500:75 V4 testdata/Builtins.lc 500:46-500:55 'Nat -> Type->Type testdata/Builtins.lc 500:35-500:75 'Nat testdata/Builtins.lc 500:35-500:75 V2 testdata/Builtins.lc 500:1-500:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 500:10-500:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 501:35-501:75 Type testdata/Builtins.lc 501:35-501:38 Type->Type testdata/Builtins.lc 501:35-501:75 V5 testdata/Builtins.lc 501:35-501:75 V4 testdata/Builtins.lc 501:46-501:55 'Nat -> Type->Type testdata/Builtins.lc 501:35-501:75 'Nat testdata/Builtins.lc 501:35-501:75 V2 testdata/Builtins.lc 501:1-501:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 501:11-501:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 502:35-502:89 Type testdata/Builtins.lc 502:35-502:89 V5 testdata/Builtins.lc 502:39-502:48 'Nat -> Type->Type testdata/Builtins.lc 502:35-502:89 'Nat testdata/Builtins.lc 502:35-502:89 V3 testdata/Builtins.lc 502:51-502:56 Type testdata/Builtins.lc 502:35-502:89 V2 testdata/Builtins.lc 502:62-502:71 'Nat -> Type->Type testdata/Builtins.lc 502:74-502:78 Type testdata/Builtins.lc 502:1-502:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 502:12-502:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 503:35-503:73 Type testdata/Builtins.lc 503:35-503:41 Type->Type testdata/Builtins.lc 503:35-503:73 V5 testdata/Builtins.lc 503:35-503:73 V4 testdata/Builtins.lc 503:49-503:58 'Nat -> Type->Type testdata/Builtins.lc 503:35-503:73 'Nat testdata/Builtins.lc 503:35-503:73 V2 testdata/Builtins.lc 503:1-503:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 503:10-503:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 504:35-504:72 Type testdata/Builtins.lc 504:35-504:72 V3 testdata/Builtins.lc 504:39-504:48 'Nat -> Type->Type testdata/Builtins.lc 504:35-504:72 'Nat testdata/Builtins.lc 504:35-504:72 V1 testdata/Builtins.lc 504:51-504:56 Type testdata/Builtins.lc 504:66-504:72 Type -> Type->Type testdata/Builtins.lc 504:1-504:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a testdata/Builtins.lc 505:35-505:80 Type testdata/Builtins.lc 505:35-505:38 Type->Type testdata/Builtins.lc 505:35-505:80 V5 testdata/Builtins.lc 505:35-505:80 V4 testdata/Builtins.lc 505:46-505:55 'Nat -> Type->Type testdata/Builtins.lc 505:35-505:80 'Nat testdata/Builtins.lc 505:35-505:80 V2 testdata/Builtins.lc 505:1-505:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b testdata/Builtins.lc 506:35-506:80 Type testdata/Builtins.lc 506:35-506:38 Type->Type testdata/Builtins.lc 506:35-506:80 V5 testdata/Builtins.lc 506:35-506:80 V4 testdata/Builtins.lc 506:46-506:55 'Nat -> Type->Type testdata/Builtins.lc 506:35-506:80 'Nat testdata/Builtins.lc 506:35-506:80 V2 testdata/Builtins.lc 506:1-506:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b testdata/Builtins.lc 507:35-507:77 Type testdata/Builtins.lc 507:35-507:77 V3 testdata/Builtins.lc 507:39-507:48 'Nat -> Type->Type testdata/Builtins.lc 507:35-507:77 'Nat testdata/Builtins.lc 507:35-507:77 V1 testdata/Builtins.lc 507:51-507:56 Type testdata/Builtins.lc 507:1-507:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 508:35-508:81 Type testdata/Builtins.lc 508:35-508:81 V3 testdata/Builtins.lc 508:39-508:48 'Nat -> Type->Type testdata/Builtins.lc 508:35-508:81 'Nat testdata/Builtins.lc 508:35-508:81 V1 testdata/Builtins.lc 508:51-508:56 Type testdata/Builtins.lc 508:71-508:76 Type testdata/Builtins.lc 508:1-508:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a testdata/Builtins.lc 509:35-509:99 Type testdata/Builtins.lc 509:35-509:99 V5 testdata/Builtins.lc 509:39-509:48 'Nat -> Type->Type testdata/Builtins.lc 509:35-509:99 'Nat testdata/Builtins.lc 509:35-509:99 V3 testdata/Builtins.lc 509:51-509:56 Type testdata/Builtins.lc 509:35-509:99 V2 testdata/Builtins.lc 509:62-509:71 'Nat -> Type->Type testdata/Builtins.lc 509:74-509:78 Type testdata/Builtins.lc 509:1-509:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a testdata/Builtins.lc 510:35-510:68 Type testdata/Builtins.lc 510:35-510:68 V3 testdata/Builtins.lc 510:39-510:44 'Nat -> Type->Type testdata/Builtins.lc 510:35-510:68 'Nat testdata/Builtins.lc 510:35-510:68 V1 testdata/Builtins.lc 510:47-510:52 Type testdata/Builtins.lc 510:1-510:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a testdata/Builtins.lc 511:35-511:76 Type testdata/Builtins.lc 511:35-511:76 V3 testdata/Builtins.lc 511:39-511:48 'Nat -> Type->Type testdata/Builtins.lc 511:35-511:76 'Nat testdata/Builtins.lc 511:35-511:76 V1 testdata/Builtins.lc 511:51-511:56 Type testdata/Builtins.lc 511:61-511:66 Type testdata/Builtins.lc 511:1-511:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a testdata/Builtins.lc 512:35-512:73 Type testdata/Builtins.lc 512:35-512:73 V3 testdata/Builtins.lc 512:39-512:44 'Nat -> Type->Type testdata/Builtins.lc 512:35-512:73 'Nat testdata/Builtins.lc 512:35-512:73 V1 testdata/Builtins.lc 512:47-512:52 Type testdata/Builtins.lc 512:1-512:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a testdata/Builtins.lc 513:35-513:85 Type testdata/Builtins.lc 513:35-513:85 V3 testdata/Builtins.lc 513:39-513:48 'Nat -> Type->Type testdata/Builtins.lc 513:35-513:85 'Nat testdata/Builtins.lc 513:35-513:85 V1 testdata/Builtins.lc 513:51-513:56 Type testdata/Builtins.lc 513:61-513:66 Type testdata/Builtins.lc 513:70-513:75 Type testdata/Builtins.lc 513:1-513:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a testdata/Builtins.lc 516:34-516:70 Type testdata/Builtins.lc 516:34-516:43 'Nat -> Type->Type testdata/Builtins.lc 516:34-516:70 'Nat testdata/Builtins.lc 516:34-516:70 V1 testdata/Builtins.lc 516:46-516:51 Type testdata/Builtins.lc 516:55-516:64 'Nat -> Type->Type testdata/Builtins.lc 516:67-516:70 Type testdata/Builtins.lc 516:1-516:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int testdata/Builtins.lc 517:34-517:71 Type testdata/Builtins.lc 517:34-517:43 'Nat -> Type->Type testdata/Builtins.lc 517:34-517:71 'Nat testdata/Builtins.lc 517:34-517:71 V1 testdata/Builtins.lc 517:46-517:51 Type testdata/Builtins.lc 517:55-517:64 'Nat -> Type->Type testdata/Builtins.lc 517:67-517:71 Type testdata/Builtins.lc 517:1-517:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word testdata/Builtins.lc 518:34-518:72 Type testdata/Builtins.lc 518:34-518:43 'Nat -> Type->Type testdata/Builtins.lc 518:34-518:72 'Nat testdata/Builtins.lc 518:34-518:72 V1 testdata/Builtins.lc 518:46-518:49 Type testdata/Builtins.lc 518:55-518:64 'Nat -> Type->Type testdata/Builtins.lc 518:67-518:72 Type testdata/Builtins.lc 518:1-518:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float testdata/Builtins.lc 519:34-519:72 Type testdata/Builtins.lc 519:34-519:43 'Nat -> Type->Type testdata/Builtins.lc 519:34-519:72 'Nat testdata/Builtins.lc 519:34-519:72 V1 testdata/Builtins.lc 519:46-519:50 Type testdata/Builtins.lc 519:55-519:64 'Nat -> Type->Type testdata/Builtins.lc 519:67-519:72 Type testdata/Builtins.lc 519:1-519:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float testdata/Builtins.lc 521:35-521:71 Type testdata/Builtins.lc 521:35-521:71 V3 testdata/Builtins.lc 521:39-521:48 'Nat -> Type->Type testdata/Builtins.lc 521:35-521:71 'Nat testdata/Builtins.lc 521:35-521:71 V1 testdata/Builtins.lc 521:51-521:56 Type testdata/Builtins.lc 521:66-521:71 Type testdata/Builtins.lc 521:1-521:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float testdata/Builtins.lc 522:35-522:76 Type testdata/Builtins.lc 522:35-522:76 V3 testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type testdata/Builtins.lc 522:35-522:76 'Nat testdata/Builtins.lc 522:35-522:76 V1 testdata/Builtins.lc 522:51-522:56 Type testdata/Builtins.lc 522:71-522:76 Type testdata/Builtins.lc 522:1-522:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 522:15-522:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 523:35-523:72 Type testdata/Builtins.lc 523:35-523:72 V1 testdata/Builtins.lc 523:39-523:56 Type testdata/Builtins.lc 523:39-523:48 'Nat -> Type->Type testdata/Builtins.lc 523:51-523:56 Type testdata/Builtins.lc 523:1-523:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a testdata/Builtins.lc 524:35-524:67 Type testdata/Builtins.lc 524:35-524:67 V3 testdata/Builtins.lc 524:39-524:48 'Nat -> Type->Type testdata/Builtins.lc 524:35-524:67 'Nat testdata/Builtins.lc 524:35-524:67 V1 testdata/Builtins.lc 524:51-524:56 Type testdata/Builtins.lc 524:1-524:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a 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:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 525:18-525:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 526:35-526:72 Type testdata/Builtins.lc 526:35-526:72 V3 testdata/Builtins.lc 526:39-526:48 'Nat -> Type->Type testdata/Builtins.lc 526:35-526:72 'Nat testdata/Builtins.lc 526:35-526:72 V1 testdata/Builtins.lc 526:51-526:56 Type testdata/Builtins.lc 526:1-526:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 528:34-528:57 Type testdata/Builtins.lc 528:34-528:39 Type -> Type->Type testdata/Builtins.lc 528:34-528:57 V3 testdata/Builtins.lc 528:34-528:57 V1 testdata/Builtins.lc 528:48-528:53 Type -> Type->Type testdata/Builtins.lc 528:1-528:14 {a} -> {b} -> 'TFMat a b -> 'TFMat b a testdata/Builtins.lc 529:34-529:53 Type testdata/Builtins.lc 529:34-529:39 Type -> Type->Type testdata/Builtins.lc 529:34-529:53 V1 testdata/Builtins.lc 529:48-529:53 Type testdata/Builtins.lc 529:1-529:16 {a} -> 'TFMat a a -> 'Float testdata/Builtins.lc 530:34-530:57 Type testdata/Builtins.lc 530:34-530:39 Type -> Type->Type testdata/Builtins.lc 530:34-530:57 V1 testdata/Builtins.lc 530:48-530:53 Type -> Type->Type testdata/Builtins.lc 530:1-530:12 {a} -> 'TFMat a a -> 'TFMat a a testdata/Builtins.lc 531:34-531:71 Type testdata/Builtins.lc 531:34-531:71 V3 testdata/Builtins.lc 531:34-531:71 V2 testdata/Builtins.lc 531:62-531:67 Type -> Type->Type testdata/Builtins.lc 531:1-531:17 {a} -> {b} -> a -> b -> 'TFMat b a testdata/Builtins.lc 532:34-532:63 Type testdata/Builtins.lc 532:34-532:39 Type -> Type->Type testdata/Builtins.lc 532:34-532:63 V3 testdata/Builtins.lc 532:34-532:63 V1 testdata/Builtins.lc 532:1-532:14 {a} -> {b} -> 'TFMat a b -> b->a testdata/Builtins.lc 533:34-533:63 Type testdata/Builtins.lc 533:34-533:63 V3 testdata/Builtins.lc 533:48-533:53 Type -> Type->Type testdata/Builtins.lc 533:34-533:63 V2 testdata/Builtins.lc 533:1-533:14 {a} -> {b} -> a -> 'TFMat a b -> b testdata/Builtins.lc 534:34-534:71 Type testdata/Builtins.lc 534:34-534:39 Type -> Type->Type testdata/Builtins.lc 534:34-534:71 V5 testdata/Builtins.lc 534:34-534:71 V3 testdata/Builtins.lc 534:48-534:53 Type -> Type->Type testdata/Builtins.lc 534:34-534:71 V2 testdata/Builtins.lc 534:62-534:67 Type -> Type->Type testdata/Builtins.lc 534:1-534:14 {a} -> {b} -> {c} -> 'TFMat a b -> 'TFMat b c -> 'TFMat a c testdata/Builtins.lc 537:35-537:97 Type testdata/Builtins.lc 537:35-537:38 Type->Type testdata/Builtins.lc 537:35-537:97 V7 testdata/Builtins.lc 537:35-537:97 V6 testdata/Builtins.lc 537:46-537:55 'Nat -> Type->Type testdata/Builtins.lc 537:35-537:97 'Nat testdata/Builtins.lc 537:35-537:97 V4 testdata/Builtins.lc 537:35-537:97 V3 testdata/Builtins.lc 537:65-537:74 'Nat -> Type->Type testdata/Builtins.lc 537:77-537:81 Type testdata/Builtins.lc 536:1-536: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 536:15-536: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 536:34-536: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 536:51-536: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 536:73-536: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 536:85-536: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 538:35-538:76 Type testdata/Builtins.lc 538:35-538:76 V3 testdata/Builtins.lc 538:39-538:55 Type->Type testdata/Builtins.lc 538:35-538:76 V1 testdata/Builtins.lc 538:72-538:76 Type testdata/Builtins.lc 538:1-538:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 538:12-538:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 541:35-541:67 Type testdata/Builtins.lc 541:35-541:67 V3 testdata/Builtins.lc 541:39-541:48 'Nat -> Type->Type testdata/Builtins.lc 541:35-541:67 'Nat testdata/Builtins.lc 541:35-541:67 V1 testdata/Builtins.lc 541:51-541:56 Type testdata/Builtins.lc 540:1-540:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 540:11-540:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 540:21-540:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 543:34-543:60 Type testdata/Builtins.lc 543:34-543:43 'Nat -> Type->Type testdata/Builtins.lc 543:34-543:60 'Nat testdata/Builtins.lc 543:34-543:60 V1 testdata/Builtins.lc 543:46-543:51 Type testdata/Builtins.lc 543:55-543:60 Type testdata/Builtins.lc 543:1-543:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float testdata/Builtins.lc 544:34-544:66 Type testdata/Builtins.lc 544:34-544:43 'Nat -> Type->Type testdata/Builtins.lc 544:34-544:66 'Nat testdata/Builtins.lc 544:34-544:66 V1 testdata/Builtins.lc 544:46-544:51 Type testdata/Builtins.lc 544:55-544:66 Type testdata/Builtins.lc 544:55-544:58 'Nat -> Type->Type testdata/Builtins.lc 544:61-544:66 Type testdata/Builtins.lc 544:1-544:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 545:34-545:66 Type testdata/Builtins.lc 545:34-545:43 'Nat -> Type->Type testdata/Builtins.lc 545:34-545:66 'Nat testdata/Builtins.lc 545:34-545:66 V1 testdata/Builtins.lc 545:46-545:51 Type testdata/Builtins.lc 545:55-545:66 Type testdata/Builtins.lc 545:55-545:58 'Nat -> Type->Type testdata/Builtins.lc 545:61-545:66 Type testdata/Builtins.lc 545:1-545:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 546:34-546:66 Type testdata/Builtins.lc 546:34-546:43 'Nat -> Type->Type testdata/Builtins.lc 546:34-546:66 'Nat testdata/Builtins.lc 546:34-546:66 V1 testdata/Builtins.lc 546:46-546:51 Type testdata/Builtins.lc 546:55-546:66 Type testdata/Builtins.lc 546:55-546:58 'Nat -> Type->Type testdata/Builtins.lc 546:61-546:66 Type testdata/Builtins.lc 546:1-546:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 562:6-562:13 Type testdata/Builtins.lc 563:20-563:26 Type testdata/Builtins.lc 564:20-564:27 Type testdata/Builtins.lc 563:3-563:16 'String->'Texture testdata/Builtins.lc 566:20-566:23 'Nat -> Type->Type testdata/Builtins.lc 566:26-566:29 Type testdata/Builtins.lc 567:20-568:27 Type testdata/Builtins.lc 567:20-567:25 'Nat -> Type->Type testdata/Builtins.lc 567:29-567:47 Type testdata/Builtins.lc 567:29-567:34 Type->Type testdata/Builtins.lc 567:36-567:47 Type testdata/Builtins.lc 567:36-567:39 'Nat -> Type->Type testdata/Builtins.lc 567:42-567:47 Type testdata/Builtins.lc 568:20-568:27 Type testdata/Builtins.lc 566:3-566:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture testdata/Builtins.lc 570:6-570:12 Type testdata/Builtins.lc 571:5-571:16 'Filter testdata/Builtins.lc 572:5-572:17 'Filter testdata/Builtins.lc 574:6-574:14 Type testdata/Builtins.lc 575:5-575:11 'EdgeMode testdata/Builtins.lc 576:5-576:19 'EdgeMode testdata/Builtins.lc 577:5-577:16 'EdgeMode testdata/Builtins.lc 579:6-579:13 Type testdata/Builtins.lc 579:24-579:30 Type testdata/Builtins.lc 579:6-579:47 Type testdata/Builtins.lc 579:31-579:39 Type testdata/Builtins.lc 579:40-579:47 Type testdata/Builtins.lc 579:16-579:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler testdata/Builtins.lc 582:14-582:21 Type testdata/Builtins.lc 582:25-582:51 Type testdata/Builtins.lc 582:25-582:28 'Nat -> Type->Type testdata/Builtins.lc 582:31-582:36 Type testdata/Builtins.lc 582:40-582:51 Type testdata/Builtins.lc 582:40-582:43 'Nat -> Type->Type testdata/Builtins.lc 582:46-582:51 Type testdata/Builtins.lc 582:1-582:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 585:30-585:39 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 585:41-585:60 V1->V1 testdata/Builtins.lc 585:41-585: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 585:53-585:60 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float testdata/Builtins.lc 585:59-585:60 'Float testdata/Builtins.lc 585:59-585:60 'Int testdata/Builtins.lc 585:1-585: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 586:46-586:55 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 586:57-586:67 V1->V1 testdata/Builtins.lc 586:57-586: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 586:1-586: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 587:24-587:32 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 587:1-587:15 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 588:25-588:35 V2 -> V2->V2 testdata/Builtins.lc 588:25-588:35 V2->V2 testdata/Builtins.lc 588:25-588:35 V2 testdata/Builtins.lc 588:25-588:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 588:13-588:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) testdata/Builtins.lc 588:13-588:21 V4 testdata/Builtins.lc 588:1-588:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b testdata/Builtins.lc 589:15-589:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 589:1-589:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 590:14-590:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 590:1-590:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 591:19-591:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 591:1-591:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) testdata/Builtins.lc 592:19-592:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 592:1-592:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c)