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:6-68:11 Type testdata/Builtins.lc 68:14-68:16 'Swizz testdata/Builtins.lc 68:19-68:21 'Swizz testdata/Builtins.lc 68:24-68:26 'Swizz testdata/Builtins.lc 68:29-68:31 'Swizz testdata/Builtins.lc 71:27-71:56 Type testdata/Builtins.lc 71:27-71:28 V5 testdata/Builtins.lc 71:32-71:33 Type testdata/Builtins.lc 71:32-71:33 V4 testdata/Builtins.lc 71:38-71:56 Type testdata/Builtins.lc 71:38-71:41 'Nat -> Type->Type testdata/Builtins.lc 71:42-71:43 'Nat testdata/Builtins.lc 71:42-71:43 V2 testdata/Builtins.lc 71:44-71:45 Type testdata/Builtins.lc 71:49-71:56 Type testdata/Builtins.lc 71:49-71:52 'Nat -> Type->Type testdata/Builtins.lc 71:53-71:54 'Nat testdata/Builtins.lc 71:55-71:56 Type testdata/Builtins.lc 72:24-75:44 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 72:24-75:44 {a} -> {b:'Nat} -> V2->a -> 'VecS V3 b -> 'VecS a b testdata/Builtins.lc 72:24-75:44 {a:'Nat} -> V2->V2 -> 'VecS V3 a -> 'VecS V3 a testdata/Builtins.lc 72:24-75:44 V2->V2 -> 'VecS V3 V1 -> 'VecS V3 V2 testdata/Builtins.lc 72:24-75:44 'VecS V3 V1 -> 'VecS V3 V2 testdata/Builtins.lc 72:24-75:44 'VecS V3 V2 testdata/Builtins.lc 72:24-72: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 72:34-72:50 a:'Nat -> 'VecS V1 a -> Type testdata/Builtins.lc 72:34-72:50 'VecS V1 V0 -> Type testdata/Builtins.lc 72:43-72:48 Type testdata/Builtins.lc 72:43-72:46 'Nat -> Type->Type testdata/Builtins.lc 72:47-72:48 'Nat testdata/Builtins.lc 73:6-73:28 V0 -> V1 -> 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 73:6-73:28 V1 -> 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 73:14-73:27 'VecS V6 (Succ (Succ Zero)) testdata/Builtins.lc 73:14-73:16 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 73:20-73:21 V0 testdata/Builtins.lc 73:20-73:21 V7 testdata/Builtins.lc 73:20-73:21 V2 testdata/Builtins.lc 73:26-73:27 V5 testdata/Builtins.lc 73:26-73:27 V6 testdata/Builtins.lc 74:6-74:36 V4 -> V5 -> V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 74:6-74:36 V5 -> V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 74:6-74:36 V6 -> 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 74:16-74:35 'VecS V6 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 74:16-74:18 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 74:22-74:23 V0 testdata/Builtins.lc 74:22-74:23 V7 testdata/Builtins.lc 74:28-74:29 V6 testdata/Builtins.lc 74:28-74:29 V7 testdata/Builtins.lc 74:34-74:35 V6 testdata/Builtins.lc 74:34-74:35 V7 testdata/Builtins.lc 75:6-75:44 V4 -> V5 -> V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:6-75:44 V5 -> V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:6-75:44 V6 -> V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:6-75:44 V7 -> 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:18-75:43 'VecS V7 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:18-75:20 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 75:24-75:25 V0 testdata/Builtins.lc 75:24-75:25 V8 testdata/Builtins.lc 75:30-75:31 V7 testdata/Builtins.lc 75:30-75:31 V8 testdata/Builtins.lc 75:36-75:37 V7 testdata/Builtins.lc 75:36-75:37 V8 testdata/Builtins.lc 75:42-75:43 V7 testdata/Builtins.lc 75:42-75:43 V8 testdata/Builtins.lc 72:1-72:7 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 80:27-80:48 Type testdata/Builtins.lc 80:27-80:30 'Nat -> Type->Type testdata/Builtins.lc 80:31-80:32 'Nat testdata/Builtins.lc 80:31-80:32 V1 testdata/Builtins.lc 80:27-80:48 V2 testdata/Builtins.lc 80:38-80:43 Type testdata/Builtins.lc 81:17-86:28 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 81:17-86:28 {a:'Nat} -> 'VecS V1 a -> 'Swizz->V3 testdata/Builtins.lc 81:17-86:28 'VecS V1 V0 -> 'Swizz->V3 testdata/Builtins.lc 81:17-86:28 'Swizz->V3 testdata/Builtins.lc 81:17-86:28 V3 testdata/Builtins.lc 81:22-81:24 V1 -> V2->V2 testdata/Builtins.lc 81:22-81:24 V2->V2 testdata/Builtins.lc 81:22-81:24 V2 testdata/Builtins.lc 81:22-81:24 'Swizz testdata/Builtins.lc 83:24-83:26 V0 -> V1 -> V2->V3 testdata/Builtins.lc 83:24-83:26 V1 -> V2->V3 testdata/Builtins.lc 83:24-83:26 V2->V3 testdata/Builtins.lc 83:24-83:26 V3 testdata/Builtins.lc 83:24-83:26 'Swizz testdata/Builtins.lc 86:26-86:28 V0 -> V1 -> V2 -> V3->V4 testdata/Builtins.lc 86:26-86:28 V1 -> V2 -> V3->V4 testdata/Builtins.lc 86:26-86:28 V2 -> V3->V4 testdata/Builtins.lc 86:26-86:28 V3->V4 testdata/Builtins.lc 86:26-86:28 V4 testdata/Builtins.lc 86:26-86:28 'Swizz testdata/Builtins.lc 81:17-81:20 'VecS V1 V0 testdata/Builtins.lc 81:17-81:20 'VecS V5 V4 testdata/Builtins.lc 81:1-81:12 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 92:28-92:43 Type testdata/Builtins.lc 92:28-92:31 'Nat -> Type->Type testdata/Builtins.lc 92:32-92:33 'Nat testdata/Builtins.lc 92:32-92:33 V1 testdata/Builtins.lc 92:34-92:35 Type testdata/Builtins.lc 92:34-92:35 V2 testdata/Builtins.lc 92:39-92:43 Type testdata/Builtins.lc 93:16-95:31 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 93:16-95:31 {a:'Nat} -> 'VecS V1 a -> 'Bool testdata/Builtins.lc 93:16-95:31 'VecS V1 V0 -> 'Bool testdata/Builtins.lc 93:16-95:31 'Bool testdata/Builtins.lc 93:23-93:27 V1 -> V2->V2 testdata/Builtins.lc 93:23-93:27 V2->V2 testdata/Builtins.lc 93:23-93:27 V2 testdata/Builtins.lc 93:23-93:27 'Bool testdata/Builtins.lc 94:25-94:29 V0 -> V1 -> V2->'Bool testdata/Builtins.lc 94:25-94:29 V1 -> V2->'Bool testdata/Builtins.lc 94:25-94:29 V2->'Bool testdata/Builtins.lc 94:25-94:29 'Bool testdata/Builtins.lc 95:27-95:31 V0 -> V1 -> V2 -> V3->'Bool testdata/Builtins.lc 95:27-95:31 V1 -> V2 -> V3->'Bool testdata/Builtins.lc 95:27-95:31 V2 -> V3->'Bool testdata/Builtins.lc 95:27-95:31 V3->'Bool testdata/Builtins.lc 95:27-95:31 'Bool testdata/Builtins.lc 93:16-93:19 'VecS V1 V0 testdata/Builtins.lc 93:16-93:19 'VecS V4 V3 testdata/Builtins.lc 93:1-93:11 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 97:38-97:71 Type testdata/Builtins.lc 97:38-97:41 'Nat -> Type->Type testdata/Builtins.lc 97:42-97:43 'Nat testdata/Builtins.lc 97:42-97:43 V3 testdata/Builtins.lc 97:38-97:71 V4 testdata/Builtins.lc 97:49-97:52 'Nat -> Type->Type testdata/Builtins.lc 97:53-97:54 'Nat testdata/Builtins.lc 97:53-97:54 V2 testdata/Builtins.lc 97:55-97:60 Type testdata/Builtins.lc 97:64-97:67 'Nat -> Type->Type testdata/Builtins.lc 97:68-97:69 'Nat testdata/Builtins.lc 98:19-98:53 {a} -> {b:'Nat} -> {c:'Nat} -> 'VecS a b -> 'VecS 'Swizz c -> 'VecS a c testdata/Builtins.lc 98:19-98:53 {a:'Nat} -> {b:'Nat} -> 'VecS V2 a -> 'VecS 'Swizz b -> 'VecS V4 b testdata/Builtins.lc 98:19-98:53 {a:'Nat} -> 'VecS V2 V1 -> 'VecS 'Swizz a -> 'VecS V4 a testdata/Builtins.lc 98:19-98:53 'VecS V2 V1 -> 'VecS 'Swizz V1 -> 'VecS V4 V2 testdata/Builtins.lc 98:19-98:53 'VecS 'Swizz V1 -> 'VecS V4 V2 testdata/Builtins.lc 98:19-98:53 'VecS V4 V2 testdata/Builtins.lc 98:34-98:53 V0 testdata/Builtins.lc 98:34-98:40 {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c testdata/Builtins.lc 98:42-98:53 V2->V2 testdata/Builtins.lc 98:42-98:53 {a} -> {b:'Nat} -> 'VecS a b -> 'Swizz->a testdata/Builtins.lc 98:19-98:31 'Bool testdata/Builtins.lc 98:19-98:29 {a} -> {b:'Nat} -> 'VecS a b -> 'Bool testdata/Builtins.lc 98:30-98:31 'VecS V1 V0 testdata/Builtins.lc 98:30-98:31 'VecS V6 V5 testdata/Builtins.lc 98:1-98:12 {a} -> {b:'Nat} -> {c:'Nat} -> 'VecS a b -> 'VecS 'Swizz c -> 'VecS a c testdata/Builtins.lc 105:10-106:30 V0->Type testdata/Builtins.lc 105:10-106:30 Type testdata/Builtins.lc 105:10-105:16 Type testdata/Builtins.lc 105:25-105:28 Type testdata/Builtins.lc 105:25-105:28 V1 testdata/Builtins.lc 106:10-106:30 Type testdata/Builtins.lc 106:10-106:16 Type testdata/Builtins.lc 106:25-106:30 Type testdata/Builtins.lc 103:7-103:13 Type->Type testdata/Builtins.lc 116:10-162:19 V0->Type testdata/Builtins.lc 116:10-162:19 Type testdata/Builtins.lc 116:10-116:19 Type testdata/Builtins.lc 116:20-116:24 Type testdata/Builtins.lc 116:20-116:24 V1 testdata/Builtins.lc 122:10-162:19 Type testdata/Builtins.lc 122:10-122:19 Type testdata/Builtins.lc 122:20-122:23 Type testdata/Builtins.lc 129:10-162:19 Type testdata/Builtins.lc 129:10-129:19 Type testdata/Builtins.lc 129:20-129:24 Type testdata/Builtins.lc 136:10-162:19 Type testdata/Builtins.lc 136:10-136:19 Type testdata/Builtins.lc 136:20-136:25 Type testdata/Builtins.lc 142:10-162:19 Type testdata/Builtins.lc 142:10-162:19 Type -> 'Nat->Type testdata/Builtins.lc 142:10-162:19 'Nat->Type testdata/Builtins.lc 142:10-154:19 Type testdata/Builtins.lc 142:10-154:19 'Nat->Type testdata/Builtins.lc 142:10-142:19 Type testdata/Builtins.lc 148:10-154:19 'Nat->Type testdata/Builtins.lc 148:10-154:19 Type testdata/Builtins.lc 148:10-148:19 Type testdata/Builtins.lc 154:10-154:19 'Nat->Type testdata/Builtins.lc 154:10-154:19 Type testdata/Builtins.lc 160:10-162:19 Type testdata/Builtins.lc 160:10-162:19 'Nat->Type testdata/Builtins.lc 160:10-160:19 Type testdata/Builtins.lc 161:10-162:19 'Nat->Type testdata/Builtins.lc 161:10-162:19 Type testdata/Builtins.lc 161:10-161:19 Type testdata/Builtins.lc 162:10-162:19 'Nat->Type testdata/Builtins.lc 162:10-162:19 Type testdata/Builtins.lc 142:26-142:33 Type testdata/Builtins.lc 108:7-108:16 Type->Type testdata/Builtins.lc 108:7-109:28 Type testdata/Builtins.lc 109:11-109:28 Type testdata/Builtins.lc 109:11-109:12 Type testdata/Builtins.lc 109:16-109:28 Type testdata/Builtins.lc 109:16-109:17 Type testdata/Builtins.lc 109:21-109:28 Type testdata/Builtins.lc 109:21-109:24 'Nat -> Type->Type testdata/Builtins.lc 109:27-109:28 Type testdata/Builtins.lc 116:20-163:12 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 116:20-163:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 117:10-117:12 {a:'Unit} -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 117:10-117:12 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ Zero)) testdata/Builtins.lc 117:10-117:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 122:20-163:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 123:10-123:12 {a:'Unit} -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 123:10-123:12 'Int -> 'Int -> 'VecS 'Int (Succ (Succ Zero)) testdata/Builtins.lc 123:10-123:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 129:20-163:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 130:10-130:12 {a:'Unit} -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 130:10-130:12 'Word -> 'Word -> 'VecS 'Word (Succ (Succ Zero)) testdata/Builtins.lc 130:10-130:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 136:20-163:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 137:10-137:12 {a:'Unit} -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 137:10-137:12 'Float -> 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 137:10-137:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 142:26-163:12 {a : 'Component V0} -> V1 -> V2 -> 'VecS V3 (Succ (Succ Zero)) testdata/Builtins.lc 143:10-163: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 143:10-163:12 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a -> 'VecS V3 a -> 'VecS ('VecS V4 a) (Succ (Succ Zero)) testdata/Builtins.lc 143:10-163:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 143:10-155:12 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 -> 'VecS 'Float V2 -> 'VecS ('VecS 'Float V3) (Succ (Succ Zero)) testdata/Builtins.lc 143:10-155: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 143:10-155: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 143:10-155: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 143:10-155: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 143:10-143: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 143:10-143:12 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS ('VecS 'Float (Succ (Succ Zero))) (Succ (Succ Zero)) testdata/Builtins.lc 143:10-143:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 149:10-155: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 149:10-155: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 149:10-149: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 149:10-149: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 149:10-149:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 155:10-155: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 155:10-155: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 155:10-155: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 155:10-155: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 155:10-155:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 163:10-163:12 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 -> 'VecS V3 V2 -> 'VecS ('VecS V4 V3) (Succ (Succ Zero)) testdata/Builtins.lc 163:10-163:12 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 -> 'VecS 'Bool V2 -> 'VecS ('VecS 'Bool V3) (Succ (Succ Zero)) testdata/Builtins.lc 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163: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 163:10-163:12 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 109:3-109:7 {a} -> {b : 'Component a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 108:7-110:33 Type testdata/Builtins.lc 110:11-110:33 Type testdata/Builtins.lc 110:11-110:12 Type testdata/Builtins.lc 110:16-110:33 Type testdata/Builtins.lc 110:16-110:17 Type testdata/Builtins.lc 110:21-110:33 Type testdata/Builtins.lc 110:21-110:22 Type testdata/Builtins.lc 110:26-110:33 Type testdata/Builtins.lc 110:26-110:29 'Nat -> Type->Type testdata/Builtins.lc 110:32-110:33 Type testdata/Builtins.lc 116:20-164:12 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 116:20-164:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 118:10-118:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 118:10-118:12 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ Zero))) testdata/Builtins.lc 118:10-118:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 122:20-164:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 124:10-124:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 124:10-124:12 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ Zero))) testdata/Builtins.lc 124:10-124:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 129:20-164:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 131:10-131:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 131:10-131:12 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ Zero))) testdata/Builtins.lc 131:10-131:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 136:20-164:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 138:10-138:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 138:10-138:12 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 138:10-138:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 142:26-164:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> 'VecS V4 (Succ (Succ (Succ Zero))) testdata/Builtins.lc 144:10-164: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 144:10-164: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 144:10-164: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 144:10-156: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 144:10-156: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 144:10-156: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 144:10-156: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 144:10-156: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 144:10-144: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 144:10-144: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 144:10-144:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 150:10-156: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 150:10-156: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 150:10-150: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 150:10-150: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 150:10-150:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 156:10-156: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 156:10-156: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 156:10-156: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 156:10-156: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 156:10-156:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164: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 164:10-164:12 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 110:3-110:7 {a} -> {b : 'Component a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 108:7-111:38 Type testdata/Builtins.lc 111:11-111:38 Type testdata/Builtins.lc 111:11-111:12 Type testdata/Builtins.lc 111:16-111:38 Type testdata/Builtins.lc 111:16-111:17 Type testdata/Builtins.lc 111:21-111:38 Type testdata/Builtins.lc 111:21-111:22 Type testdata/Builtins.lc 111:26-111:38 Type testdata/Builtins.lc 111:26-111:27 Type testdata/Builtins.lc 111:31-111:38 Type testdata/Builtins.lc 111:31-111:34 'Nat -> Type->Type testdata/Builtins.lc 111:37-111:38 Type testdata/Builtins.lc 116:20-165:12 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 116:20-165:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 119:10-119:12 {a:'Unit} -> 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 119:10-119:12 'Bool -> 'Bool -> 'Bool -> 'Bool -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 119:10-119:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 122:20-165:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 125:10-125:12 {a:'Unit} -> 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 125:10-125:12 'Int -> 'Int -> 'Int -> 'Int -> 'VecS 'Int (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 125:10-125:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 129:20-165:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 132:10-132:12 {a:'Unit} -> 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 132:10-132:12 'Word -> 'Word -> 'Word -> 'Word -> 'VecS 'Word (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 132:10-132:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 136:20-165:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 139:10-139:12 {a:'Unit} -> 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 139:10-139:12 'Float -> 'Float -> 'Float -> 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 139:10-139:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 142:26-165:12 {a : 'Component V0} -> V1 -> V2 -> V3 -> V4 -> 'VecS V5 (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 145:10-165: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 145:10-165: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 145:10-165: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 145:10-157: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 145:10-157: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 145:10-157: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 145:10-157: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 145:10-157: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 145:10-145: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 145:10-145: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 145:10-145:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 151:10-157: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 151:10-157: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 151:10-151: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 151:10-151: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 151:10-151:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 157:10-157: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 157:10-157: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 157:10-157: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 157:10-157: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 157:10-157:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165: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 165:10-165:12 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 111:3-111:7 {a} -> {b : 'Component a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 108:7-112:16 Type testdata/Builtins.lc 112:15-112:16 Type testdata/Builtins.lc 116:20-166:40 {a} -> {b : 'Component a}->a testdata/Builtins.lc 116:20-166:40 {a : 'Component V0}->V1 testdata/Builtins.lc 120:14-120:19 {a:'Unit}->'Bool testdata/Builtins.lc 120:14-120:19 'Bool testdata/Builtins.lc 122:20-166:40 {a : 'Component V0}->V1 testdata/Builtins.lc 126:14-126:22 {a:'Unit}->'Int testdata/Builtins.lc 126:19-126:22 Type testdata/Builtins.lc 126:14-126:15 'Int testdata/Builtins.lc 129:20-166:40 {a : 'Component V0}->V1 testdata/Builtins.lc 133:14-133:23 {a:'Unit}->'Word testdata/Builtins.lc 133:19-133:23 Type testdata/Builtins.lc 133:14-133:15 'Word testdata/Builtins.lc 133:14-133:15 'Int testdata/Builtins.lc 136:20-166:40 {a : 'Component V0}->V1 testdata/Builtins.lc 140:14-140:17 {a:'Unit}->'Float testdata/Builtins.lc 140:14-140:17 'Float testdata/Builtins.lc 142:26-166:40 {a : 'Component V0}->V1 testdata/Builtins.lc 146:14-166:40 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 146:14-166:40 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 146:14-166:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 146:14-158:32 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 146:14-158:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 146:14-158:32 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 146:14-158:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 146:14-158:32 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 146:14-146:24 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 146:14-146:16 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 146:17-146:20 V0 testdata/Builtins.lc 146:17-146:20 'Float testdata/Builtins.lc 146:21-146:24 'Float testdata/Builtins.lc 152:14-158:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 152:14-158:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 152:14-152:28 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 152:14-152:16 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 152:17-152:20 V0 testdata/Builtins.lc 152:17-152:20 'Float testdata/Builtins.lc 152:21-152:24 'Float testdata/Builtins.lc 152:25-152:28 'Float testdata/Builtins.lc 158:14-158:32 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 158:14-158:32 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 158:14-158:32 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 158:14-158:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 158:17-158:20 V0 testdata/Builtins.lc 158:17-158:20 'Float testdata/Builtins.lc 158:21-158:24 'Float testdata/Builtins.lc 158:25-158:28 'Float testdata/Builtins.lc 158:29-158:32 'Float testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 166:14-166:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 166:14-166:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 166:14-166:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 166:14-166:40 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 166:14-166:40 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 166:14-166:40 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 166:14-166:16 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 166:17-166:22 V0 testdata/Builtins.lc 166:17-166:22 'Bool testdata/Builtins.lc 166:23-166:28 'Bool testdata/Builtins.lc 166:29-166:34 'Bool testdata/Builtins.lc 166:35-166:40 'Bool testdata/Builtins.lc 112:3-112:11 {a} -> {b : 'Component a}->a testdata/Builtins.lc 108:7-113:15 Type testdata/Builtins.lc 113:14-113:15 Type testdata/Builtins.lc 116:20-167:35 {a} -> {b : 'Component a}->a testdata/Builtins.lc 116:20-167:35 {a : 'Component V0}->V1 testdata/Builtins.lc 121:13-121:17 {a:'Unit}->'Bool testdata/Builtins.lc 121:13-121:17 'Bool testdata/Builtins.lc 122:20-167:35 {a : 'Component V0}->V1 testdata/Builtins.lc 127:13-127:21 {a:'Unit}->'Int testdata/Builtins.lc 127:18-127:21 Type testdata/Builtins.lc 127:13-127:14 'Int testdata/Builtins.lc 129:20-167:35 {a : 'Component V0}->V1 testdata/Builtins.lc 134:13-134:22 {a:'Unit}->'Word testdata/Builtins.lc 134:18-134:22 Type testdata/Builtins.lc 134:13-134:14 'Word testdata/Builtins.lc 134:13-134:14 'Int testdata/Builtins.lc 136:20-167:35 {a : 'Component V0}->V1 testdata/Builtins.lc 141:13-141:16 {a:'Unit}->'Float testdata/Builtins.lc 141:13-141:16 'Float testdata/Builtins.lc 142:26-167:35 {a : 'Component V0}->V1 testdata/Builtins.lc 147:13-167:35 a:Type -> b:'Nat -> {c : 'Component ('VecS a b)} -> 'VecS a b testdata/Builtins.lc 147:13-167:35 a:'Nat -> {b : 'Component ('VecS V1 a)} -> 'VecS V2 a testdata/Builtins.lc 147:13-167:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 147:13-159:31 {a : 'Component ('VecS 'Float V0)} -> 'VecS 'Float V1 testdata/Builtins.lc 147:13-159:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ a))} -> 'VecS 'Float (Succ a) testdata/Builtins.lc 147:13-159:31 {a : 'Component ('VecS 'Float (Succ V0))} -> 'VecS 'Float (Succ V1) testdata/Builtins.lc 147:13-159:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ a)))} -> 'VecS 'Float (Succ (Succ a)) testdata/Builtins.lc 147:13-159:31 {a : 'Component ('VecS 'Float (Succ (Succ V0)))} -> 'VecS 'Float (Succ (Succ V1)) testdata/Builtins.lc 147:13-147:23 {a:'Unit} -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 147:13-147:15 {a} -> a -> a -> 'VecS a (Succ (Succ Zero)) testdata/Builtins.lc 147:16-147:19 V0 testdata/Builtins.lc 147:16-147:19 'Float testdata/Builtins.lc 147:20-147:23 'Float testdata/Builtins.lc 153:13-159:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ a))))} -> 'VecS 'Float (Succ (Succ (Succ a))) testdata/Builtins.lc 153:13-159:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ V0))))} -> 'VecS 'Float (Succ (Succ (Succ V1))) testdata/Builtins.lc 153:13-153:27 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 153:13-153:15 {a} -> a -> a -> a -> 'VecS a (Succ (Succ (Succ Zero))) testdata/Builtins.lc 153:16-153:19 V0 testdata/Builtins.lc 153:16-153:19 'Float testdata/Builtins.lc 153:20-153:23 'Float testdata/Builtins.lc 153:24-153:27 'Float testdata/Builtins.lc 159:13-159:31 a:'Nat -> {b : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 159:13-159:31 {a : 'Component ('VecS 'Float (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Float (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 159:13-159:31 {a:'Unit} -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 159:13-159:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 159:16-159:19 V0 testdata/Builtins.lc 159:16-159:19 'Float testdata/Builtins.lc 159:20-159:23 'Float testdata/Builtins.lc 159:24-159:27 'Float testdata/Builtins.lc 159:28-159:31 'Float testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS V1 V0)} -> 'VecS V2 V1 testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS 'Bool V0)} -> 'VecS 'Bool V1 testdata/Builtins.lc 167:13-167:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ a))} -> 'VecS 'Bool (Succ a) testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS 'Bool (Succ V0))} -> 'VecS 'Bool (Succ V1) testdata/Builtins.lc 167:13-167:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ a)))} -> 'VecS 'Bool (Succ (Succ a)) testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS 'Bool (Succ (Succ V0)))} -> 'VecS 'Bool (Succ (Succ V1)) testdata/Builtins.lc 167:13-167:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ a))))} -> 'VecS 'Bool (Succ (Succ (Succ a))) testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ V0))))} -> 'VecS 'Bool (Succ (Succ (Succ V1))) testdata/Builtins.lc 167:13-167:35 a:'Nat -> {b : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ a)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ a)))) testdata/Builtins.lc 167:13-167:35 {a : 'Component ('VecS 'Bool (Succ (Succ (Succ (Succ V0)))))} -> 'VecS 'Bool (Succ (Succ (Succ (Succ V1)))) testdata/Builtins.lc 167:13-167:35 {a:'Unit} -> 'VecS 'Bool (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:13-167:15 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 167:16-167:20 V0 testdata/Builtins.lc 167:16-167:20 'Bool testdata/Builtins.lc 167:21-167:25 'Bool testdata/Builtins.lc 167:26-167:30 'Bool testdata/Builtins.lc 167:31-167:35 'Bool testdata/Builtins.lc 113:3-113:10 {a} -> {b : 'Component a}->a testdata/Builtins.lc 171:10-172:29 V0->Type testdata/Builtins.lc 171:10-172:29 Type testdata/Builtins.lc 171:10-171:18 Type testdata/Builtins.lc 171:25-171:28 Type testdata/Builtins.lc 171:25-171:28 V1 testdata/Builtins.lc 172:10-172:29 Type testdata/Builtins.lc 172:10-172:18 Type testdata/Builtins.lc 172:25-172:29 Type testdata/Builtins.lc 169:7-169:15 Type->Type testdata/Builtins.lc 176:10-188:18 V0->Type testdata/Builtins.lc 176:10-188:18 Type testdata/Builtins.lc 176:10-176:18 Type testdata/Builtins.lc 176:25-176:30 Type testdata/Builtins.lc 176:25-176:30 V1 testdata/Builtins.lc 177:10-188:18 Type testdata/Builtins.lc 177:10-179:18 Type -> 'Nat->Type testdata/Builtins.lc 177:10-179:18 'Nat->Type testdata/Builtins.lc 177:10-179:18 Type testdata/Builtins.lc 177:10-177:18 Type testdata/Builtins.lc 178:10-179:18 'Nat->Type testdata/Builtins.lc 178:10-179:18 Type testdata/Builtins.lc 178:10-178:18 Type testdata/Builtins.lc 179:10-179:18 'Nat->Type testdata/Builtins.lc 179:10-179:18 Type testdata/Builtins.lc 177:31-177:38 Type testdata/Builtins.lc 180:10-188:18 Type testdata/Builtins.lc 180:10-188:18 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 180:10-188:18 'Nat -> Type->Type testdata/Builtins.lc 180:10-188:18 Type->Type testdata/Builtins.lc 180:10-188:18 'Nat->Type testdata/Builtins.lc 180:10-182:18 Type testdata/Builtins.lc 180:10-182:18 'Nat->Type testdata/Builtins.lc 180:10-180:18 Type testdata/Builtins.lc 181:10-182:18 'Nat->Type testdata/Builtins.lc 181:10-182:18 Type testdata/Builtins.lc 181:10-181:18 Type testdata/Builtins.lc 182:10-182:18 'Nat->Type testdata/Builtins.lc 182:10-182:18 Type testdata/Builtins.lc 183:10-188:18 'Nat->Type testdata/Builtins.lc 183:10-188:18 Type testdata/Builtins.lc 183:10-185:18 Type testdata/Builtins.lc 183:10-185:18 'Nat->Type testdata/Builtins.lc 183:10-183:18 Type testdata/Builtins.lc 184:10-185:18 'Nat->Type testdata/Builtins.lc 184:10-185:18 Type testdata/Builtins.lc 184:10-184:18 Type testdata/Builtins.lc 185:10-185:18 'Nat->Type testdata/Builtins.lc 185:10-185:18 Type testdata/Builtins.lc 186:10-188:18 'Nat->Type testdata/Builtins.lc 186:10-188:18 Type testdata/Builtins.lc 186:10-186:18 Type testdata/Builtins.lc 187:10-188:18 'Nat->Type testdata/Builtins.lc 187:10-188:18 Type testdata/Builtins.lc 187:10-187:18 Type testdata/Builtins.lc 188:10-188:18 'Nat->Type testdata/Builtins.lc 188:10-188:18 Type testdata/Builtins.lc 180:30-180:39 Type testdata/Builtins.lc 174:7-174:15 Type->Type testdata/Builtins.lc 190:6-190:20 Type testdata/Builtins.lc 191:7-191:12 'BlendingFactor testdata/Builtins.lc 192:7-192:10 'BlendingFactor testdata/Builtins.lc 193:7-193:15 'BlendingFactor testdata/Builtins.lc 194:7-194:23 'BlendingFactor testdata/Builtins.lc 195:7-195:15 'BlendingFactor testdata/Builtins.lc 196:7-196:23 '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:20 'BlendingFactor testdata/Builtins.lc 202:7-202:28 'BlendingFactor testdata/Builtins.lc 203:7-203:20 'BlendingFactor testdata/Builtins.lc 204:7-204:28 'BlendingFactor testdata/Builtins.lc 205:7-205:23 'BlendingFactor testdata/Builtins.lc 207:6-207:19 Type testdata/Builtins.lc 208:7-208:14 'BlendEquation testdata/Builtins.lc 209:7-209:19 'BlendEquation testdata/Builtins.lc 210:7-210:26 'BlendEquation testdata/Builtins.lc 211:7-211:10 'BlendEquation testdata/Builtins.lc 212:7-212:10 'BlendEquation testdata/Builtins.lc 214:6-214:20 Type testdata/Builtins.lc 215:7-215:12 'LogicOperation testdata/Builtins.lc 216:7-216:10 'LogicOperation testdata/Builtins.lc 217:7-217:17 'LogicOperation testdata/Builtins.lc 218:7-218:11 'LogicOperation testdata/Builtins.lc 219:7-219:18 'LogicOperation testdata/Builtins.lc 220:7-220:11 'LogicOperation testdata/Builtins.lc 221:7-221:10 'LogicOperation testdata/Builtins.lc 222:7-222:9 'LogicOperation testdata/Builtins.lc 223:7-223:10 'LogicOperation testdata/Builtins.lc 224:7-224:12 'LogicOperation testdata/Builtins.lc 225:7-225:13 'LogicOperation testdata/Builtins.lc 226:7-226:16 'LogicOperation testdata/Builtins.lc 227:7-227:19 'LogicOperation testdata/Builtins.lc 228:7-228:17 'LogicOperation testdata/Builtins.lc 229:7-229:11 'LogicOperation testdata/Builtins.lc 230:7-230:10 'LogicOperation testdata/Builtins.lc 232:6-232:22 Type testdata/Builtins.lc 233:7-233:13 'StencilOperation testdata/Builtins.lc 234:7-234:13 'StencilOperation testdata/Builtins.lc 235:7-235:16 'StencilOperation testdata/Builtins.lc 236:7-236:13 'StencilOperation testdata/Builtins.lc 237:7-237:17 'StencilOperation testdata/Builtins.lc 238:7-238:13 'StencilOperation testdata/Builtins.lc 239:7-239:17 'StencilOperation testdata/Builtins.lc 240:7-240:15 'StencilOperation testdata/Builtins.lc 242:6-242:24 Type testdata/Builtins.lc 243:7-243:12 'ComparisonFunction testdata/Builtins.lc 244:7-244:11 'ComparisonFunction testdata/Builtins.lc 245:7-245:12 'ComparisonFunction testdata/Builtins.lc 246:7-246:13 'ComparisonFunction testdata/Builtins.lc 247:7-247:14 'ComparisonFunction testdata/Builtins.lc 248:7-248:15 'ComparisonFunction testdata/Builtins.lc 249:7-249:13 'ComparisonFunction testdata/Builtins.lc 250:7-250:13 'ComparisonFunction testdata/Builtins.lc 252:6-252:21 Type testdata/Builtins.lc 253:7-253:17 'ProvokingVertex testdata/Builtins.lc 254:7-254:18 'ProvokingVertex testdata/Builtins.lc 256:6-256:14 Type testdata/Builtins.lc 257:7-257:16 'CullMode testdata/Builtins.lc 258:7-258:15 'CullMode testdata/Builtins.lc 259:7-259:15 'CullMode testdata/Builtins.lc 261:6-261:15 Type testdata/Builtins.lc 262:17-262:22 Type testdata/Builtins.lc 262:7-262:16 'Float->'PointSize testdata/Builtins.lc 263:7-263:23 'PointSize testdata/Builtins.lc 265:6-265:17 Type testdata/Builtins.lc 266:7-266:18 'PolygonMode testdata/Builtins.lc 267:20-267:29 Type testdata/Builtins.lc 267:7-267:19 'PointSize->'PolygonMode testdata/Builtins.lc 268:19-268:24 Type testdata/Builtins.lc 268:7-268:18 'Float->'PolygonMode testdata/Builtins.lc 270:6-270:19 Type testdata/Builtins.lc 271:7-271:15 'PolygonOffset testdata/Builtins.lc 272:14-272:19 Type testdata/Builtins.lc 270:6-272:25 Type testdata/Builtins.lc 272:20-272:25 Type testdata/Builtins.lc 272:7-272:13 'Float -> 'Float->'PolygonOffset testdata/Builtins.lc 274:6-274:28 Type testdata/Builtins.lc 275:7-275:16 'PointSpriteCoordOrigin testdata/Builtins.lc 276:7-276:16 'PointSpriteCoordOrigin testdata/Builtins.lc 279:6-279:11 Type->Type testdata/Builtins.lc 280:6-280:13 Type->Type testdata/Builtins.lc 281:6-281:11 Type->Type testdata/Builtins.lc 283:6-283:19 Type testdata/Builtins.lc 284:7-284:15 'PrimitiveType testdata/Builtins.lc 285:7-285:11 'PrimitiveType testdata/Builtins.lc 286:7-286:12 'PrimitiveType testdata/Builtins.lc 287:7-287:24 'PrimitiveType testdata/Builtins.lc 288:7-288:20 'PrimitiveType testdata/Builtins.lc 291:16-291:18 Type testdata/Builtins.lc 291:22-291:48 Type testdata/Builtins.lc 291:22-291:25 'Nat -> Type->Type testdata/Builtins.lc 291:28-291:33 Type testdata/Builtins.lc 291:37-291:48 Type testdata/Builtins.lc 291:37-291:40 'Nat -> Type->Type testdata/Builtins.lc 291:43-291:48 Type testdata/Builtins.lc 291:1-291:12 'Tuple0 -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 294:14-294:25 Type testdata/Builtins.lc 294:14-294:20 Type testdata/Builtins.lc 294:14-294:25 V2 testdata/Builtins.lc 294:1-294:8 {a} -> 'String->a testdata/Builtins.lc 295:14-295:25 Type testdata/Builtins.lc 295:14-295:20 Type testdata/Builtins.lc 295:14-295:25 V2 testdata/Builtins.lc 295:1-295:10 {a} -> 'String->a testdata/Builtins.lc 297:23-297:36 Type testdata/Builtins.lc 297:40-297:44 Type testdata/Builtins.lc 297:6-297:19 'PrimitiveType->Type testdata/Builtins.lc 298:26-298:34 Type testdata/Builtins.lc 298:38-298:111 Type testdata/Builtins.lc 298:38-298:49 Type testdata/Builtins.lc 298:53-298:111 Type testdata/Builtins.lc 298:53-298:66 Type testdata/Builtins.lc 298:70-298:111 Type testdata/Builtins.lc 298:70-298:85 Type testdata/Builtins.lc 298:89-298:111 Type testdata/Builtins.lc 298:89-298:102 'PrimitiveType->Type testdata/Builtins.lc 298:103-298:111 'PrimitiveType testdata/Builtins.lc 298:3-298:14 'CullMode -> 'PolygonMode -> 'PolygonOffset -> 'ProvokingVertex -> 'RasterContext Triangle testdata/Builtins.lc 299:26-299:35 Type testdata/Builtins.lc 299:39-299:108 Type testdata/Builtins.lc 299:39-299:44 Type testdata/Builtins.lc 299:48-299:108 Type testdata/Builtins.lc 299:48-299:70 Type testdata/Builtins.lc 299:89-299:108 Type testdata/Builtins.lc 299:89-299:102 'PrimitiveType->Type testdata/Builtins.lc 299:103-299:108 'PrimitiveType testdata/Builtins.lc 299:3-299:11 'PointSize -> 'Float -> 'PointSpriteCoordOrigin -> 'RasterContext Point testdata/Builtins.lc 300:26-300:31 Type testdata/Builtins.lc 300:35-300:107 Type testdata/Builtins.lc 300:35-300:50 Type testdata/Builtins.lc 300:89-300:107 Type testdata/Builtins.lc 300:89-300:102 'PrimitiveType->Type testdata/Builtins.lc 300:103-300:107 'PrimitiveType testdata/Builtins.lc 300:3-300:10 'Float -> 'ProvokingVertex -> 'RasterContext Line testdata/Builtins.lc 298:103-300:107 Type testdata/Builtins.lc 298:103-298:111 Type testdata/Builtins.lc 299:103-300:107 Type testdata/Builtins.lc 299:103-299:108 Type testdata/Builtins.lc 300:103-300:107 Type testdata/Builtins.lc 302:6-302:18 Type->Type testdata/Builtins.lc 304:27-304:56 Type testdata/Builtins.lc 304:27-304:35 Type->Type testdata/Builtins.lc 304:36-304:37 Type testdata/Builtins.lc 304:42-304:56 Type testdata/Builtins.lc 304:42-304:54 Type->Type testdata/Builtins.lc 304:55-304:56 Type testdata/Builtins.lc 303:3-303:9 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 303:11-303:24 {a} -> {b : 'Floating a} -> 'Interpolated a testdata/Builtins.lc 305:42-305:56 Type testdata/Builtins.lc 305:42-305:54 Type->Type testdata/Builtins.lc 305:55-305:56 Type testdata/Builtins.lc 305:3-305:7 {a} -> 'Interpolated a testdata/Builtins.lc 309:14-310:32 Type->Type testdata/Builtins.lc 309:14-310:32 Type testdata/Builtins.lc 309:14-309:15 Type testdata/Builtins.lc 310:15-310:32 Type testdata/Builtins.lc 310:26-310:32 Type -> Type->Type testdata/Builtins.lc 310:26-310:32 Type->Type testdata/Builtins.lc 310:26-310:32 Type testdata/Builtins.lc 310:15-310:21 Type testdata/Builtins.lc 309:5-309:12 Type->Type testdata/Builtins.lc 313:27-316:82 Type->Type testdata/Builtins.lc 313:27-316:82 Type testdata/Builtins.lc 313:27-313:29 Type testdata/Builtins.lc 314:36-316:82 Type testdata/Builtins.lc 314:36-314:37 Type testdata/Builtins.lc 315:23-316:82 Type testdata/Builtins.lc 315:57-315:63 Type -> Type->Type testdata/Builtins.lc 315:57-315:63 Type->Type testdata/Builtins.lc 315:57-315:63 Type testdata/Builtins.lc 315:23-315:53 Type testdata/Builtins.lc 316:23-316:82 Type testdata/Builtins.lc 316:73-316:82 Type -> Type -> Type->Type testdata/Builtins.lc 316:73-316:82 Type -> Type->Type testdata/Builtins.lc 316:73-316:82 Type->Type testdata/Builtins.lc 316:73-316:82 Type testdata/Builtins.lc 316:23-316:69 Type testdata/Builtins.lc 313:5-313:21 Type->Type testdata/Builtins.lc 318:18-318:22 Type testdata/Builtins.lc 318:26-318:30 Type testdata/Builtins.lc 318:6-318:14 Type->Type testdata/Builtins.lc 319:60-319:70 Type testdata/Builtins.lc 319:60-319:68 Type->Type testdata/Builtins.lc 319:60-319:70 V1 testdata/Builtins.lc 319:3-319:13 {a} -> 'Blending a testdata/Builtins.lc 320:27-320:70 Type testdata/Builtins.lc 320:27-320:35 Type->Type testdata/Builtins.lc 320:27-320:70 V1 testdata/Builtins.lc 320:42-320:56 Type testdata/Builtins.lc 320:60-320:68 Type->Type testdata/Builtins.lc 320:3-320:15 {a} -> {b : 'Integral a} -> 'LogicOperation -> 'Blending a testdata/Builtins.lc 321:26-321:56 Type -> Type->Type testdata/Builtins.lc 321:27-321:40 Type testdata/Builtins.lc 321:42-321:55 Type testdata/Builtins.lc 322:29-323:74 Type testdata/Builtins.lc 322:29-322:97 Type -> Type->Type testdata/Builtins.lc 322:30-322:62 Type testdata/Builtins.lc 322:30-322:62 Type -> Type->Type testdata/Builtins.lc 322:31-322:45 Type testdata/Builtins.lc 322:47-322:61 Type testdata/Builtins.lc 322:64-322:96 Type testdata/Builtins.lc 322:64-322:96 Type -> Type->Type testdata/Builtins.lc 322:65-322:79 Type testdata/Builtins.lc 322:81-322:95 Type testdata/Builtins.lc 323:29-323:74 Type testdata/Builtins.lc 323:29-323:32 'Nat -> Type->Type testdata/Builtins.lc 323:35-323:40 Type testdata/Builtins.lc 323:60-323:74 Type testdata/Builtins.lc 323:60-323:68 Type->Type testdata/Builtins.lc 323:69-323:74 Type testdata/Builtins.lc 321:3-321:8 'Tuple2 'BlendEquation 'BlendEquation -> 'Tuple2 ('Tuple2 'BlendingFactor 'BlendingFactor) ('Tuple2 'BlendingFactor 'BlendingFactor) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Blending 'Float testdata/Builtins.lc 319:60-323:74 Type testdata/Builtins.lc 320:27-323:74 Type testdata/Builtins.lc 330:6-330:18 Type testdata/Builtins.lc 331:6-331:16 Type testdata/Builtins.lc 332:6-332:11 Type testdata/Builtins.lc 334:27-334:31 Type testdata/Builtins.lc 334:35-334:39 Type testdata/Builtins.lc 334:6-334:23 Type->Type testdata/Builtins.lc 335:27-336:101 Type testdata/Builtins.lc 335:27-336:101 V7 testdata/Builtins.lc 335:34-335:43 'Nat -> Type->Type testdata/Builtins.lc 335:27-336:101 'Nat testdata/Builtins.lc 335:27-336:101 V5 testdata/Builtins.lc 335:46-335:50 Type testdata/Builtins.lc 335:27-336:101 V4 testdata/Builtins.lc 335:60-335:69 'Nat -> Type->Type testdata/Builtins.lc 335:27-336:101 V2 testdata/Builtins.lc 335:75-335:78 Type->Type testdata/Builtins.lc 335:85-335:93 Type->Type testdata/Builtins.lc 336:71-336:88 Type->Type testdata/Builtins.lc 336:90-336:95 Type->Type testdata/Builtins.lc 335:3-335: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 337:26-337:44 Type testdata/Builtins.lc 337:48-337:101 Type testdata/Builtins.lc 337:48-337:52 Type testdata/Builtins.lc 337:71-337:101 Type testdata/Builtins.lc 337:71-337:88 Type->Type testdata/Builtins.lc 337:90-337:101 Type testdata/Builtins.lc 337:90-337:95 Type->Type testdata/Builtins.lc 337:96-337:101 Type testdata/Builtins.lc 337:3-337:10 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 338:26-338:38 Type testdata/Builtins.lc 338:42-338:103 Type testdata/Builtins.lc 338:42-338:52 Type testdata/Builtins.lc 338:56-338:103 Type testdata/Builtins.lc 338:56-338:66 Type testdata/Builtins.lc 338:71-338:103 Type testdata/Builtins.lc 338:71-338:88 Type->Type testdata/Builtins.lc 338:90-338:103 Type testdata/Builtins.lc 338:90-338:97 Type->Type testdata/Builtins.lc 338:98-338:103 Type testdata/Builtins.lc 338:3-338:12 'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation ('Stencil 'Int32) testdata/Builtins.lc 335:27-338:103 Type testdata/Builtins.lc 337:90-338:103 Type testdata/Builtins.lc 341:32-345:146 Type->Type testdata/Builtins.lc 341:32-345:146 Type testdata/Builtins.lc 341:32-341:33 Type testdata/Builtins.lc 342:14-345:146 Type testdata/Builtins.lc 342:60-342:68 Type -> Type->Type testdata/Builtins.lc 342:60-342:68 Type->Type testdata/Builtins.lc 342:60-342:68 Type testdata/Builtins.lc 342:14-342:56 Type testdata/Builtins.lc 343:14-345:146 Type testdata/Builtins.lc 343:82-343:94 Type -> Type -> Type->Type testdata/Builtins.lc 343:82-343:94 Type -> Type->Type testdata/Builtins.lc 343:82-343:94 Type->Type testdata/Builtins.lc 343:82-343:94 Type testdata/Builtins.lc 343:14-343:78 Type testdata/Builtins.lc 344:14-345:146 Type testdata/Builtins.lc 344:104-344:120 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 344:104-344:120 Type -> Type -> Type->Type testdata/Builtins.lc 344:104-344:120 Type -> Type->Type testdata/Builtins.lc 344:104-344:120 Type->Type testdata/Builtins.lc 344:104-344:120 Type testdata/Builtins.lc 344:14-344:100 Type testdata/Builtins.lc 345:14-345:146 Type testdata/Builtins.lc 345:126-345:146 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 345:126-345:146 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 345:126-345:146 Type -> Type -> Type->Type testdata/Builtins.lc 345:126-345:146 Type -> Type->Type testdata/Builtins.lc 345:126-345:146 Type->Type testdata/Builtins.lc 345:126-345:146 Type testdata/Builtins.lc 345:14-345:122 Type testdata/Builtins.lc 341:5-341:12 Type->Type testdata/Builtins.lc 348:15-352:36 Type->Type testdata/Builtins.lc 348:15-352:36 Type testdata/Builtins.lc 348:25-348:69 Type -> Type->Type testdata/Builtins.lc 348:25-348:69 Type->Type testdata/Builtins.lc 348:25-348:69 Type testdata/Builtins.lc 348:26-348:43 Type testdata/Builtins.lc 348:26-348:43 Type->Type testdata/Builtins.lc 348:48-348:65 Type testdata/Builtins.lc 348:48-348:65 Type->Type testdata/Builtins.lc 348:15-348:21 Type testdata/Builtins.lc 349:15-352:36 Type testdata/Builtins.lc 349:29-349:95 Type -> Type -> Type->Type testdata/Builtins.lc 349:29-349:95 Type -> Type->Type testdata/Builtins.lc 349:29-349:95 Type->Type testdata/Builtins.lc 349:29-349:95 Type testdata/Builtins.lc 349:30-349:47 Type testdata/Builtins.lc 349:30-349:47 Type->Type testdata/Builtins.lc 349:52-349:69 Type testdata/Builtins.lc 349:52-349:69 Type->Type testdata/Builtins.lc 349:74-349:91 Type testdata/Builtins.lc 349:74-349:91 Type->Type testdata/Builtins.lc 349:15-349:25 Type testdata/Builtins.lc 350:15-352:36 Type testdata/Builtins.lc 350:34-350:122 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 350:34-350:122 Type -> Type -> Type->Type testdata/Builtins.lc 350:34-350:122 Type -> Type->Type testdata/Builtins.lc 350:34-350:122 Type->Type testdata/Builtins.lc 350:34-350:122 Type testdata/Builtins.lc 350:35-350:52 Type testdata/Builtins.lc 350:35-350:52 Type->Type testdata/Builtins.lc 350:57-350:74 Type testdata/Builtins.lc 350:57-350:74 Type->Type testdata/Builtins.lc 350:79-350:96 Type testdata/Builtins.lc 350:79-350:96 Type->Type testdata/Builtins.lc 350:101-350:118 Type testdata/Builtins.lc 350:101-350:118 Type->Type testdata/Builtins.lc 350:15-350:29 Type testdata/Builtins.lc 351:15-352:36 Type testdata/Builtins.lc 351:38-351:148 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 351:38-351:148 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 351:38-351:148 Type -> Type -> Type->Type testdata/Builtins.lc 351:38-351:148 Type -> Type->Type testdata/Builtins.lc 351:38-351:148 Type->Type testdata/Builtins.lc 351:38-351:148 Type testdata/Builtins.lc 351:39-351:56 Type testdata/Builtins.lc 351:39-351:56 Type->Type testdata/Builtins.lc 351:61-351:78 Type testdata/Builtins.lc 351:61-351:78 Type->Type testdata/Builtins.lc 351:83-351:100 Type testdata/Builtins.lc 351:83-351:100 Type->Type testdata/Builtins.lc 351:105-351:122 Type testdata/Builtins.lc 351:105-351:122 Type->Type testdata/Builtins.lc 351:127-351:144 Type testdata/Builtins.lc 351:127-351:144 Type->Type testdata/Builtins.lc 351:15-351:33 Type testdata/Builtins.lc 352:19-352:36 Type testdata/Builtins.lc 352:19-352:36 Type->Type testdata/Builtins.lc 348:5-348:13 Type->Type testdata/Builtins.lc 354:6-354:12 Type->Type testdata/Builtins.lc 356:15-356:46 Type testdata/Builtins.lc 356:15-356:46 V3 testdata/Builtins.lc 356:15-356:46 V2 testdata/Builtins.lc 356:26-356:32 Type->Type testdata/Builtins.lc 356:38-356:44 Type->Type testdata/Builtins.lc 356:1-356:10 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 357:18-357:52 Type testdata/Builtins.lc 357:18-357:52 V1 testdata/Builtins.lc 357:23-357:27 Type testdata/Builtins.lc 357:32-357:38 Type->Type testdata/Builtins.lc 357:44-357:50 Type->Type testdata/Builtins.lc 357:1-357:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 359:22-359:35 Type testdata/Builtins.lc 359:6-359:15 'PrimitiveType -> Type->Type testdata/Builtins.lc 361:18-361:59 Type testdata/Builtins.lc 361:18-361:59 V5 testdata/Builtins.lc 361:18-361:59 V4 testdata/Builtins.lc 361:29-361:38 'PrimitiveType -> Type->Type testdata/Builtins.lc 361:18-361:59 'PrimitiveType testdata/Builtins.lc 361:18-361:59 V2 testdata/Builtins.lc 361:46-361:55 'PrimitiveType -> Type->Type testdata/Builtins.lc 361:1-361:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 363:39-363:96 Type testdata/Builtins.lc 363:39-363:53 {a} -> a->Type testdata/Builtins.lc 363:54-363:55 V0 testdata/Builtins.lc 363:54-363:55 V2 testdata/Builtins.lc 363:60-363:96 Type testdata/Builtins.lc 363:60-363:66 Type testdata/Builtins.lc 363:70-363:96 Type testdata/Builtins.lc 363:70-363:71 V3 testdata/Builtins.lc 363:75-363:96 Type testdata/Builtins.lc 363:75-363:81 Type->Type testdata/Builtins.lc 363:83-363:96 Type testdata/Builtins.lc 363:83-363:92 'PrimitiveType -> Type->Type testdata/Builtins.lc 363:93-363:94 'PrimitiveType testdata/Builtins.lc 363:93-363:94 V5 testdata/Builtins.lc 363:95-363:96 Type testdata/Builtins.lc 363:1-363:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 364:42-364:106 Type testdata/Builtins.lc 364:42-364:56 {a} -> a->Type testdata/Builtins.lc 364:57-364:58 V0 testdata/Builtins.lc 364:57-364:58 V4 testdata/Builtins.lc 364:60-364:106 Type testdata/Builtins.lc 364:60-364:61 Type testdata/Builtins.lc 364:60-364:61 V4 testdata/Builtins.lc 364:64-364:74 Type testdata/Builtins.lc 364:64-364:71 Type->Type testdata/Builtins.lc 364:72-364:74 Type testdata/Builtins.lc 364:72-364:74 V2 testdata/Builtins.lc 364:79-364:106 Type testdata/Builtins.lc 364:79-364:81 Type testdata/Builtins.lc 364:85-364:106 Type testdata/Builtins.lc 364:85-364:91 Type->Type testdata/Builtins.lc 364:93-364:106 Type testdata/Builtins.lc 364:93-364:102 'PrimitiveType -> Type->Type testdata/Builtins.lc 364:103-364:104 'PrimitiveType testdata/Builtins.lc 364:103-364:104 V6 testdata/Builtins.lc 364:105-364:106 Type testdata/Builtins.lc 364:1-364:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 366:19-366:79 Type testdata/Builtins.lc 366:19-366:79 V5 testdata/Builtins.lc 366:19-366:79 V4 testdata/Builtins.lc 366:31-366:37 Type->Type testdata/Builtins.lc 366:39-366:48 'PrimitiveType -> Type->Type testdata/Builtins.lc 366:19-366:79 'PrimitiveType testdata/Builtins.lc 366:19-366:79 V2 testdata/Builtins.lc 366:58-366:64 Type->Type testdata/Builtins.lc 366:66-366:75 'PrimitiveType -> Type->Type testdata/Builtins.lc 367:19-367:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 367:19-367:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) testdata/Builtins.lc 367:19-367:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) testdata/Builtins.lc 367:19-367:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 367:19-367:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 367:19-367:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 367:30-367:42 V1->V1 testdata/Builtins.lc 367:30-367:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 367:1-367:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 369:15-369:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 369:1-369:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) testdata/Builtins.lc 370:19-370:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 370:1-370:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) testdata/Builtins.lc 372:6-372:18 Type testdata/Builtins.lc 372:21-372:28 'DepthHandler testdata/Builtins.lc 372:31-372:43 'DepthHandler testdata/Builtins.lc 389:23-399:82 Type->Type testdata/Builtins.lc 389:23-399:82 Type testdata/Builtins.lc 389:23-389:25 Type testdata/Builtins.lc 390:25-399:82 Type testdata/Builtins.lc 390:25-390:26 Type testdata/Builtins.lc 391:19-399:82 Type testdata/Builtins.lc 391:39-391:45 Type -> Type->Type testdata/Builtins.lc 391:39-391:45 Type->Type testdata/Builtins.lc 391:39-391:45 Type testdata/Builtins.lc 391:19-391:35 Type testdata/Builtins.lc 392:19-399:82 Type testdata/Builtins.lc 392:48-397:58 Type -> Type -> Type->Type testdata/Builtins.lc 392:48-397:58 Type -> Type->Type testdata/Builtins.lc 392:48-397:58 Type->Type testdata/Builtins.lc 392:48-397:58 Type testdata/Builtins.lc 392:48-392:57 Type->Type testdata/Builtins.lc 392:48-392:57 Type testdata/Builtins.lc 392:48-392:57 Type -> Type -> Type->Type testdata/Builtins.lc 397:52-397:58 Type testdata/Builtins.lc 397:52-397:58 Type->Type testdata/Builtins.lc 397:52-397:58 Type -> Type->Type testdata/Builtins.lc 392:19-392:44 Type testdata/Builtins.lc 393:19-399:82 Type testdata/Builtins.lc 393:57-398:70 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 393:57-398:70 Type -> Type -> Type->Type testdata/Builtins.lc 393:57-398:70 Type -> Type->Type testdata/Builtins.lc 393:57-398:70 Type->Type testdata/Builtins.lc 393:57-398:70 Type testdata/Builtins.lc 393:57-393:69 Type->Type testdata/Builtins.lc 393:57-393:69 Type testdata/Builtins.lc 393:57-393:69 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 398:61-398:70 Type testdata/Builtins.lc 398:61-398:70 Type->Type testdata/Builtins.lc 398:61-398:70 Type -> Type -> Type->Type testdata/Builtins.lc 393:19-393:53 Type testdata/Builtins.lc 394:19-399:82 Type testdata/Builtins.lc 394:66-399:82 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 394:66-399:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 394:66-399:82 Type -> Type -> Type->Type testdata/Builtins.lc 394:66-399:82 Type -> Type->Type testdata/Builtins.lc 394:66-399:82 Type->Type testdata/Builtins.lc 394:66-399:82 Type testdata/Builtins.lc 394:66-394:81 Type->Type testdata/Builtins.lc 394:66-394:81 Type testdata/Builtins.lc 394:66-394:81 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 399:70-399:82 Type testdata/Builtins.lc 399:70-399:82 Type->Type testdata/Builtins.lc 399:70-399:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 394:19-394:62 Type testdata/Builtins.lc 395:25-395:36 Type testdata/Builtins.lc 395:34-395:36 Type->Type testdata/Builtins.lc 395:34-395:36 Type testdata/Builtins.lc 395:25-395:30 Type testdata/Builtins.lc 389:5-389:17 Type->Type testdata/Builtins.lc 403:18-403:21 Type testdata/Builtins.lc 403:25-403:53 Type testdata/Builtins.lc 403:25-403:37 Type testdata/Builtins.lc 403:41-403:53 Type testdata/Builtins.lc 403:41-403:45 Type testdata/Builtins.lc 403:49-403:53 Type testdata/Builtins.lc 403:6-403:14 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 405:20-405:78 Type testdata/Builtins.lc 405:20-405:78 V3 testdata/Builtins.lc 405:25-405:30 Type testdata/Builtins.lc 405:35-405:43 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 405:20-405:78 'Nat testdata/Builtins.lc 405:20-405:78 V2 testdata/Builtins.lc 405:53-405:61 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 405:64-405:76 'DepthHandler testdata/Builtins.lc 405:1-405:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 407:21-407:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 407:32-407:46 V1->V1 testdata/Builtins.lc 407:32-407:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 407:1-407:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) testdata/Builtins.lc 414:21-418:62 Type testdata/Builtins.lc 414:21-418:62 V7 testdata/Builtins.lc 414:25-414:41 Type->Type testdata/Builtins.lc 414:21-418:62 V5 testdata/Builtins.lc 414:21-418:62 V4 testdata/Builtins.lc 414:49-414:62 Type -> Type->Type testdata/Builtins.lc 414:64-414:75 Type testdata/Builtins.lc 414:64-414:67 'Nat -> Type->Type testdata/Builtins.lc 414:70-414:75 Type testdata/Builtins.lc 415:26-415:31 Type testdata/Builtins.lc 417:20-417:33 'PrimitiveType->Type testdata/Builtins.lc 414:21-418:62 'PrimitiveType testdata/Builtins.lc 418:20-418:29 'PrimitiveType -> Type->Type testdata/Builtins.lc 418:37-418:45 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 418:48-418:60 'DepthHandler testdata/Builtins.lc 414:1-414: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 420:20-420:56 Type testdata/Builtins.lc 420:20-420:56 V3 testdata/Builtins.lc 420:25-420:29 Type testdata/Builtins.lc 420:34-420:42 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 420:20-420:56 'Nat testdata/Builtins.lc 420:20-420:56 V2 testdata/Builtins.lc 420:52-420:56 Type testdata/Builtins.lc 420:1-420:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 422:21-422:84 Type testdata/Builtins.lc 422:21-422:84 V5 testdata/Builtins.lc 422:26-422:30 Type testdata/Builtins.lc 422:35-422:41 Type->Type testdata/Builtins.lc 422:43-422:51 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 422:21-422:84 'Nat testdata/Builtins.lc 422:21-422:84 V4 testdata/Builtins.lc 422:21-422:84 'DepthHandler testdata/Builtins.lc 422:21-422:84 V2 testdata/Builtins.lc 422:62-422:68 Type->Type testdata/Builtins.lc 422:70-422:78 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 423:21-423:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 423:21-423:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) testdata/Builtins.lc 423:21-423:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) testdata/Builtins.lc 423:21-423:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 423:21-423:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 423:21-423:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 423:35-423:49 V0->'Bool testdata/Builtins.lc 423:35-423:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 423:1-423:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 425:17-425:60 Type testdata/Builtins.lc 425:17-425:60 V7 testdata/Builtins.lc 425:17-425:60 V6 testdata/Builtins.lc 425:28-425:36 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 425:17-425:60 'Nat testdata/Builtins.lc 425:17-425:60 V4 testdata/Builtins.lc 425:17-425:60 'DepthHandler testdata/Builtins.lc 425:17-425:60 V2 testdata/Builtins.lc 425:46-425:54 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 425:1-425:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 427:18-427:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 427:29-427:40 V1->V1 testdata/Builtins.lc 427:29-427:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 427:1-427:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 432:13-432:26 Type->Type testdata/Builtins.lc 437:13-437:28 Type->Type testdata/Builtins.lc 440:10-441:36 V0->Type testdata/Builtins.lc 440:10-441:36 Type testdata/Builtins.lc 440:10-440:23 Type->Type testdata/Builtins.lc 440:10-440:23 Type testdata/Builtins.lc 440:10-440:23 Type -> 'Nat->Type testdata/Builtins.lc 440:10-440:23 'Nat->Type testdata/Builtins.lc 440:37-440:44 Type testdata/Builtins.lc 440:37-440:44 V1 testdata/Builtins.lc 441:10-441:36 Type testdata/Builtins.lc 441:10-441:23 Type->Type testdata/Builtins.lc 441:10-441:23 Type testdata/Builtins.lc 441:31-441:36 Type testdata/Builtins.lc 439:7-439:20 Type->Type testdata/Builtins.lc 439:7-439:65 Type testdata/Builtins.lc 439:46-439:65 Type testdata/Builtins.lc 439:46-439:63 Type->Type testdata/Builtins.lc 439:64-439:65 Type testdata/Builtins.lc 440:37-441:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a testdata/Builtins.lc 440:37-441:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 testdata/Builtins.lc 440:69-440:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) testdata/Builtins.lc 440:69-440:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) testdata/Builtins.lc 440:69-440:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) testdata/Builtins.lc 440:69-440:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) testdata/Builtins.lc 440:69-440:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) testdata/Builtins.lc 440:69-440:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) testdata/Builtins.lc 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) testdata/Builtins.lc 440:69-440: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 440:69-440:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) testdata/Builtins.lc 440:69-440:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) testdata/Builtins.lc 440:69-440: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 440:77-440:87 'Blending V1 testdata/Builtins.lc 440:77-440:87 {a} -> 'Blending a testdata/Builtins.lc 440:89-440:111 'VecScalar V2 'Bool testdata/Builtins.lc 440:89-440:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 440:92-440:96 V0 testdata/Builtins.lc 440:92-440:96 'Bool testdata/Builtins.lc 440:97-440:101 'Bool testdata/Builtins.lc 440:102-440:106 'Bool testdata/Builtins.lc 440:107-440:111 'Bool testdata/Builtins.lc 441:31-441:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 testdata/Builtins.lc 441:60-441:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) testdata/Builtins.lc 441:60-441:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) testdata/Builtins.lc 441:60-441:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 441:60-441:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 441:68-441:72 'ComparisonFunction testdata/Builtins.lc 441:73-441:77 'Bool testdata/Builtins.lc 439:29-439:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b testdata/Builtins.lc 448:24-448:27 Type testdata/Builtins.lc 448:6-448:17 'Nat -> Type->Type testdata/Builtins.lc 449:19-449:109 Type testdata/Builtins.lc 449:19-449:27 Type->Type testdata/Builtins.lc 449:28-449:29 Type testdata/Builtins.lc 449:33-449:39 Type->Type testdata/Builtins.lc 449:41-449:49 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 449:50-449:51 'Nat testdata/Builtins.lc 449:19-449:109 'DepthHandler testdata/Builtins.lc 449:19-449:109 V2 testdata/Builtins.lc 449:55-449:69 Type testdata/Builtins.lc 449:55-449:67 Type->Type testdata/Builtins.lc 449:68-449:69 Type testdata/Builtins.lc 449:75-449:109 Type testdata/Builtins.lc 449:75-449:86 'Nat -> Type->Type testdata/Builtins.lc 449:87-449:88 'Nat testdata/Builtins.lc 449:89-449:90 Type testdata/Builtins.lc 449:94-449:109 Type testdata/Builtins.lc 449:94-449:105 'Nat -> Type->Type testdata/Builtins.lc 449:106-449:107 'Nat testdata/Builtins.lc 449:108-449:109 Type testdata/Builtins.lc 449:3-449:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 450:20-450:117 Type testdata/Builtins.lc 450:20-450:36 {a} -> a->Type testdata/Builtins.lc 450:37-450:38 V0 testdata/Builtins.lc 450:37-450:38 Type testdata/Builtins.lc 450:40-450:55 Type->Type testdata/Builtins.lc 450:20-450:117 V2 testdata/Builtins.lc 450:59-450:74 Type testdata/Builtins.lc 450:59-450:70 'Nat -> Type->Type testdata/Builtins.lc 450:71-450:72 'Nat testdata/Builtins.lc 450:73-450:74 Type testdata/Builtins.lc 450:77-450:90 Type->Type testdata/Builtins.lc 450:102-450:117 Type testdata/Builtins.lc 450:102-450:113 'Nat -> Type->Type testdata/Builtins.lc 450:114-450:115 'Nat testdata/Builtins.lc 450:116-450:117 Type testdata/Builtins.lc 450:3-450:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 452:34-452:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 452:50-452:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) testdata/Builtins.lc 452:50-452:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 452:1-452: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 454:1-454:20 {a} -> a->a testdata/Builtins.lc 456:15-456:18 Type testdata/Builtins.lc 456:22-456:34 Type testdata/Builtins.lc 456:22-456:26 Type testdata/Builtins.lc 456:30-456:34 Type testdata/Builtins.lc 456:6-456:11 'Nat -> Type->Type testdata/Builtins.lc 457:48-458:56 Type testdata/Builtins.lc 457:48-457:51 Type->Type testdata/Builtins.lc 457:52-457:53 Type testdata/Builtins.lc 457:52-457:53 V3 testdata/Builtins.lc 457:55-458:56 Type testdata/Builtins.lc 457:55-457:60 Type testdata/Builtins.lc 457:55-457:60 V2 testdata/Builtins.lc 457:63-457:76 Type testdata/Builtins.lc 457:63-457:72 'Nat -> Type->Type testdata/Builtins.lc 457:73-457:74 'Nat testdata/Builtins.lc 457:73-457:74 V4 testdata/Builtins.lc 457:75-457:76 Type testdata/Builtins.lc 458:26-458:56 Type testdata/Builtins.lc 458:26-458:31 Type testdata/Builtins.lc 458:36-458:56 Type testdata/Builtins.lc 458:36-458:41 'Nat -> Type->Type testdata/Builtins.lc 458:42-458:43 'Nat testdata/Builtins.lc 458:42-458:43 V7 testdata/Builtins.lc 458:45-458:56 Type testdata/Builtins.lc 458:45-458:50 Type->Type testdata/Builtins.lc 458:51-458:56 Type testdata/Builtins.lc 457:3-457:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 459:37-459:67 Type testdata/Builtins.lc 459:37-459:42 Type testdata/Builtins.lc 459:47-459:67 Type testdata/Builtins.lc 459:47-459:52 'Nat -> Type->Type testdata/Builtins.lc 459:53-459:54 'Nat testdata/Builtins.lc 459:53-459:54 V2 testdata/Builtins.lc 459:56-459:67 Type testdata/Builtins.lc 459:56-459:61 Type->Type testdata/Builtins.lc 459:62-459:67 Type testdata/Builtins.lc 459:3-459:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 460:37-460:67 Type testdata/Builtins.lc 460:37-460:40 Type testdata/Builtins.lc 460:47-460:67 Type testdata/Builtins.lc 460:47-460:52 'Nat -> Type->Type testdata/Builtins.lc 460:53-460:54 'Nat testdata/Builtins.lc 460:53-460:54 V2 testdata/Builtins.lc 460:56-460:67 Type testdata/Builtins.lc 460:56-460:63 Type->Type testdata/Builtins.lc 460:64-460:67 Type testdata/Builtins.lc 460:3-460:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) testdata/Builtins.lc 463:26-463:54 Type testdata/Builtins.lc 463:26-463:37 'Nat -> Type->Type testdata/Builtins.lc 463:26-463:54 V1 testdata/Builtins.lc 463:45-463:50 'Nat -> Type->Type testdata/Builtins.lc 463:3-463:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a testdata/Builtins.lc 464:26-464:37 'Nat -> Type->Type testdata/Builtins.lc 464:40-464:74 Type testdata/Builtins.lc 464:40-464:74 Type -> Type->Type testdata/Builtins.lc 464:41-464:52 Type testdata/Builtins.lc 464:41-464:46 Type->Type testdata/Builtins.lc 464:47-464:52 Type testdata/Builtins.lc 464:54-464:72 Type testdata/Builtins.lc 464:54-464:59 Type->Type testdata/Builtins.lc 464:61-464:72 Type testdata/Builtins.lc 464:61-464:64 'Nat -> Type->Type testdata/Builtins.lc 464:67-464:72 Type testdata/Builtins.lc 464:78-464:105 Type testdata/Builtins.lc 464:78-464:83 'Nat -> Type->Type testdata/Builtins.lc 464:87-464:105 Type testdata/Builtins.lc 464:87-464:92 Type->Type testdata/Builtins.lc 464:94-464:105 Type testdata/Builtins.lc 464:94-464:97 'Nat -> Type->Type testdata/Builtins.lc 464:100-464:105 Type testdata/Builtins.lc 464:3-464: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 458:42-464:105 Type testdata/Builtins.lc 458:42-458:56 Type testdata/Builtins.lc 459:53-464:105 Type testdata/Builtins.lc 459:53-459:67 Type testdata/Builtins.lc 460:53-464:105 Type testdata/Builtins.lc 460:53-460:67 Type testdata/Builtins.lc 463:26-464:105 Type testdata/Builtins.lc 466:6-466:12 Type testdata/Builtins.lc 467:26-467:51 Type testdata/Builtins.lc 467:26-467:37 'Nat -> Type->Type testdata/Builtins.lc 467:26-467:51 'Nat testdata/Builtins.lc 467:26-467:51 V3 testdata/Builtins.lc 467:26-467:51 V1 testdata/Builtins.lc 467:45-467:51 Type testdata/Builtins.lc 467:3-467:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 473:34-473:73 Type testdata/Builtins.lc 473:34-473:37 Type->Type testdata/Builtins.lc 473:39-473:55 Type->Type testdata/Builtins.lc 473:34-473:73 V1 testdata/Builtins.lc 473:1-473:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 473:10-473:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 473:19-473:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 474:35-474:80 Type testdata/Builtins.lc 474:35-474:80 V3 testdata/Builtins.lc 474:39-474:55 Type->Type testdata/Builtins.lc 474:35-474:80 V1 testdata/Builtins.lc 474:59-474:62 Type->Type testdata/Builtins.lc 474:1-474:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 474:11-474:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 474:21-474:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 475:35-475:75 Type testdata/Builtins.lc 475:35-475:38 Type->Type testdata/Builtins.lc 475:35-475:75 V5 testdata/Builtins.lc 475:35-475:75 V4 testdata/Builtins.lc 475:46-475:55 'Nat -> Type->Type testdata/Builtins.lc 475:35-475:75 'Nat testdata/Builtins.lc 475:35-475:75 V2 testdata/Builtins.lc 475:1-475:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 475:10-475:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 476:35-476:75 Type testdata/Builtins.lc 476:35-476:38 Type->Type testdata/Builtins.lc 476:35-476:75 V5 testdata/Builtins.lc 476:35-476:75 V4 testdata/Builtins.lc 476:46-476:55 'Nat -> Type->Type testdata/Builtins.lc 476:35-476:75 'Nat testdata/Builtins.lc 476:35-476:75 V2 testdata/Builtins.lc 476:1-476:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 476:11-476:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 477:34-477:71 Type testdata/Builtins.lc 477:34-477:40 Type->Type testdata/Builtins.lc 477:42-477:58 Type->Type testdata/Builtins.lc 477:34-477:71 V1 testdata/Builtins.lc 477:1-477:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a testdata/Builtins.lc 479:35-479:80 Type testdata/Builtins.lc 479:35-479:43 Type->Type testdata/Builtins.lc 479:35-479:80 V5 testdata/Builtins.lc 479:35-479:80 V4 testdata/Builtins.lc 479:51-479:60 'Nat -> Type->Type testdata/Builtins.lc 479:35-479:80 'Nat testdata/Builtins.lc 479:35-479:80 V2 testdata/Builtins.lc 479:1-479:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 479:11-479:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 479:20-479:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 480:35-480:80 Type testdata/Builtins.lc 480:35-480:43 Type->Type testdata/Builtins.lc 480:35-480:80 V5 testdata/Builtins.lc 480:35-480:80 V4 testdata/Builtins.lc 480:51-480:60 'Nat -> Type->Type testdata/Builtins.lc 480:35-480:80 'Nat testdata/Builtins.lc 480:35-480:80 V2 testdata/Builtins.lc 480:1-480:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 480:12-480:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 480:22-480:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 481:35-481:75 Type testdata/Builtins.lc 481:35-481:43 Type->Type testdata/Builtins.lc 481:35-481:75 V5 testdata/Builtins.lc 481:35-481:75 V4 testdata/Builtins.lc 481:51-481:60 'Nat -> Type->Type testdata/Builtins.lc 481:35-481:75 'Nat testdata/Builtins.lc 481:35-481:75 V2 testdata/Builtins.lc 481:1-481:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 482:35-482:102 Type testdata/Builtins.lc 482:35-482:43 Type->Type testdata/Builtins.lc 482:35-482:102 V7 testdata/Builtins.lc 482:35-482:102 V6 testdata/Builtins.lc 482:51-482:60 'Nat -> Type->Type testdata/Builtins.lc 482:35-482:102 'Nat testdata/Builtins.lc 482:35-482:102 V4 testdata/Builtins.lc 482:35-482:102 V3 testdata/Builtins.lc 482:70-482:79 'Nat -> Type->Type testdata/Builtins.lc 482:82-482:86 Type testdata/Builtins.lc 482:1-482: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 482:14-482: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 483:35-483:83 Type testdata/Builtins.lc 483:35-483:43 Type->Type testdata/Builtins.lc 483:35-483:83 V5 testdata/Builtins.lc 483:35-483:83 V4 testdata/Builtins.lc 483:51-483:60 'Nat -> Type->Type testdata/Builtins.lc 483:35-483:83 'Nat testdata/Builtins.lc 483:35-483:83 V2 testdata/Builtins.lc 483:74-483:78 Type testdata/Builtins.lc 483:1-483:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 483:15-483:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 485:34-485:38 Type testdata/Builtins.lc 485:42-485:54 Type testdata/Builtins.lc 485:42-485:46 Type testdata/Builtins.lc 485:50-485:54 Type testdata/Builtins.lc 485:1-485:8 'Bool -> 'Bool->'Bool testdata/Builtins.lc 485:10-485:16 'Bool -> 'Bool->'Bool testdata/Builtins.lc 485:18-485:25 'Bool -> 'Bool->'Bool testdata/Builtins.lc 486:35-486:66 Type testdata/Builtins.lc 486:35-486:66 V3 testdata/Builtins.lc 486:39-486:48 'Nat -> Type->Type testdata/Builtins.lc 486:35-486:66 'Nat testdata/Builtins.lc 486:35-486:66 V1 testdata/Builtins.lc 486:51-486:55 Type testdata/Builtins.lc 486:1-486:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a testdata/Builtins.lc 487:34-487:58 Type testdata/Builtins.lc 487:34-487:43 'Nat -> Type->Type testdata/Builtins.lc 487:34-487:58 'Nat testdata/Builtins.lc 487:34-487:58 V1 testdata/Builtins.lc 487:46-487:50 Type testdata/Builtins.lc 487:54-487:58 Type testdata/Builtins.lc 487:1-487:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 487:10-487:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 491:35-491:67 Type testdata/Builtins.lc 491:35-491:67 V3 testdata/Builtins.lc 491:39-491:48 'Nat -> Type->Type testdata/Builtins.lc 491:35-491:67 'Nat testdata/Builtins.lc 491:35-491:67 V1 testdata/Builtins.lc 491:51-491:56 Type testdata/Builtins.lc 490:1-490:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:11-490:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:22-490:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:32-490:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:43-490:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:53-490:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:64-490:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:73-490:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:83-490:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:96-490:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:109-490:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:118-490:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:128-490:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:137-490:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:147-490:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:156-490:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:165-490:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:175-490:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:185-490:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 490:195-490:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 492:35-492:72 Type testdata/Builtins.lc 492:35-492:72 V3 testdata/Builtins.lc 492:39-492:48 'Nat -> Type->Type testdata/Builtins.lc 492:35-492:72 'Nat testdata/Builtins.lc 492:35-492:72 V1 testdata/Builtins.lc 492:51-492:56 Type testdata/Builtins.lc 492:1-492:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 492:10-492:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a 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:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:12-494:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:23-494:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:34-494:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:49-494:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 494:59-494:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 496:35-496:75 Type testdata/Builtins.lc 496:35-496:38 Type->Type testdata/Builtins.lc 496:35-496:75 V5 testdata/Builtins.lc 496:35-496:75 V4 testdata/Builtins.lc 496:46-496:55 'Nat -> Type->Type testdata/Builtins.lc 496:35-496:75 'Nat testdata/Builtins.lc 496:35-496:75 V2 testdata/Builtins.lc 496:1-496:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 496:10-496:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 497:35-497:75 Type testdata/Builtins.lc 497:35-497:38 Type->Type testdata/Builtins.lc 497:35-497:75 V5 testdata/Builtins.lc 497:35-497:75 V4 testdata/Builtins.lc 497:46-497:55 'Nat -> Type->Type testdata/Builtins.lc 497:35-497:75 'Nat testdata/Builtins.lc 497:35-497:75 V2 testdata/Builtins.lc 497:1-497:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 497:11-497:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 498:35-498:89 Type testdata/Builtins.lc 498:35-498:89 V5 testdata/Builtins.lc 498:39-498:48 'Nat -> Type->Type testdata/Builtins.lc 498:35-498:89 'Nat testdata/Builtins.lc 498:35-498:89 V3 testdata/Builtins.lc 498:51-498:56 Type testdata/Builtins.lc 498:35-498:89 V2 testdata/Builtins.lc 498:62-498:71 'Nat -> Type->Type testdata/Builtins.lc 498:74-498:78 Type testdata/Builtins.lc 498:1-498:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 498:12-498:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 499:35-499:73 Type testdata/Builtins.lc 499:35-499:41 Type->Type testdata/Builtins.lc 499:35-499:73 V5 testdata/Builtins.lc 499:35-499:73 V4 testdata/Builtins.lc 499:49-499:58 'Nat -> Type->Type testdata/Builtins.lc 499:35-499:73 'Nat testdata/Builtins.lc 499:35-499:73 V2 testdata/Builtins.lc 499:1-499:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 499:10-499:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 500:35-500:72 Type testdata/Builtins.lc 500:35-500:72 V3 testdata/Builtins.lc 500:39-500:48 'Nat -> Type->Type testdata/Builtins.lc 500:35-500:72 'Nat testdata/Builtins.lc 500:35-500:72 V1 testdata/Builtins.lc 500:51-500:56 Type testdata/Builtins.lc 500:66-500:72 Type -> Type->Type testdata/Builtins.lc 500:1-500:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a testdata/Builtins.lc 501:35-501:80 Type testdata/Builtins.lc 501:35-501:38 Type->Type testdata/Builtins.lc 501:35-501:80 V5 testdata/Builtins.lc 501:35-501:80 V4 testdata/Builtins.lc 501:46-501:55 'Nat -> Type->Type testdata/Builtins.lc 501:35-501:80 'Nat testdata/Builtins.lc 501:35-501:80 V2 testdata/Builtins.lc 501:1-501:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b testdata/Builtins.lc 502:35-502:80 Type testdata/Builtins.lc 502:35-502:38 Type->Type testdata/Builtins.lc 502:35-502:80 V5 testdata/Builtins.lc 502:35-502:80 V4 testdata/Builtins.lc 502:46-502:55 'Nat -> Type->Type testdata/Builtins.lc 502:35-502:80 'Nat testdata/Builtins.lc 502:35-502:80 V2 testdata/Builtins.lc 502:1-502:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b testdata/Builtins.lc 503:35-503:77 Type testdata/Builtins.lc 503:35-503:77 V3 testdata/Builtins.lc 503:39-503:48 'Nat -> Type->Type testdata/Builtins.lc 503:35-503:77 'Nat testdata/Builtins.lc 503:35-503:77 V1 testdata/Builtins.lc 503:51-503:56 Type testdata/Builtins.lc 503:1-503:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 504:35-504:81 Type testdata/Builtins.lc 504:35-504:81 V3 testdata/Builtins.lc 504:39-504:48 'Nat -> Type->Type testdata/Builtins.lc 504:35-504:81 'Nat testdata/Builtins.lc 504:35-504:81 V1 testdata/Builtins.lc 504:51-504:56 Type testdata/Builtins.lc 504:71-504:76 Type testdata/Builtins.lc 504:1-504:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a testdata/Builtins.lc 505:35-505:99 Type testdata/Builtins.lc 505:35-505:99 V5 testdata/Builtins.lc 505:39-505:48 'Nat -> Type->Type testdata/Builtins.lc 505:35-505:99 'Nat testdata/Builtins.lc 505:35-505:99 V3 testdata/Builtins.lc 505:51-505:56 Type testdata/Builtins.lc 505:35-505:99 V2 testdata/Builtins.lc 505:62-505:71 'Nat -> Type->Type testdata/Builtins.lc 505:74-505:78 Type testdata/Builtins.lc 505:1-505:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a testdata/Builtins.lc 506:35-506:68 Type testdata/Builtins.lc 506:35-506:68 V3 testdata/Builtins.lc 506:39-506:44 'Nat -> Type->Type testdata/Builtins.lc 506:35-506:68 'Nat testdata/Builtins.lc 506:35-506:68 V1 testdata/Builtins.lc 506:47-506:52 Type testdata/Builtins.lc 506:1-506:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a testdata/Builtins.lc 507:35-507:76 Type testdata/Builtins.lc 507:35-507:76 V3 testdata/Builtins.lc 507:39-507:48 'Nat -> Type->Type testdata/Builtins.lc 507:35-507:76 'Nat testdata/Builtins.lc 507:35-507:76 V1 testdata/Builtins.lc 507:51-507:56 Type testdata/Builtins.lc 507:61-507:66 Type testdata/Builtins.lc 507:1-507:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a testdata/Builtins.lc 508:35-508:73 Type testdata/Builtins.lc 508:35-508:73 V3 testdata/Builtins.lc 508:39-508:44 'Nat -> Type->Type testdata/Builtins.lc 508:35-508:73 'Nat testdata/Builtins.lc 508:35-508:73 V1 testdata/Builtins.lc 508:47-508:52 Type testdata/Builtins.lc 508:1-508:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a testdata/Builtins.lc 509:35-509:85 Type testdata/Builtins.lc 509:35-509:85 V3 testdata/Builtins.lc 509:39-509:48 'Nat -> Type->Type testdata/Builtins.lc 509:35-509:85 'Nat testdata/Builtins.lc 509:35-509:85 V1 testdata/Builtins.lc 509:51-509:56 Type testdata/Builtins.lc 509:61-509:66 Type testdata/Builtins.lc 509:70-509:75 Type testdata/Builtins.lc 509:1-509:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a testdata/Builtins.lc 512:34-512:70 Type testdata/Builtins.lc 512:34-512:43 'Nat -> Type->Type testdata/Builtins.lc 512:34-512:70 'Nat testdata/Builtins.lc 512:34-512:70 V1 testdata/Builtins.lc 512:46-512:51 Type testdata/Builtins.lc 512:55-512:64 'Nat -> Type->Type testdata/Builtins.lc 512:67-512:70 Type testdata/Builtins.lc 512:1-512:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int testdata/Builtins.lc 513:34-513:71 Type testdata/Builtins.lc 513:34-513:43 'Nat -> Type->Type testdata/Builtins.lc 513:34-513:71 'Nat testdata/Builtins.lc 513:34-513:71 V1 testdata/Builtins.lc 513:46-513:51 Type testdata/Builtins.lc 513:55-513:64 'Nat -> Type->Type testdata/Builtins.lc 513:67-513:71 Type testdata/Builtins.lc 513:1-513:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word testdata/Builtins.lc 514:34-514:72 Type testdata/Builtins.lc 514:34-514:43 'Nat -> Type->Type testdata/Builtins.lc 514:34-514:72 'Nat testdata/Builtins.lc 514:34-514:72 V1 testdata/Builtins.lc 514:46-514:49 Type testdata/Builtins.lc 514:55-514:64 'Nat -> Type->Type testdata/Builtins.lc 514:67-514:72 Type testdata/Builtins.lc 514:1-514:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float testdata/Builtins.lc 515:34-515:72 Type testdata/Builtins.lc 515:34-515:43 'Nat -> Type->Type testdata/Builtins.lc 515:34-515:72 'Nat testdata/Builtins.lc 515:34-515:72 V1 testdata/Builtins.lc 515:46-515:50 Type testdata/Builtins.lc 515:55-515:64 'Nat -> Type->Type testdata/Builtins.lc 515:67-515:72 Type testdata/Builtins.lc 515:1-515:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float testdata/Builtins.lc 517:35-517:71 Type testdata/Builtins.lc 517:35-517:71 V3 testdata/Builtins.lc 517:39-517:48 'Nat -> Type->Type testdata/Builtins.lc 517:35-517:71 'Nat testdata/Builtins.lc 517:35-517:71 V1 testdata/Builtins.lc 517:51-517:56 Type testdata/Builtins.lc 517:66-517:71 Type testdata/Builtins.lc 517:1-517:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float testdata/Builtins.lc 518:35-518:76 Type testdata/Builtins.lc 518:35-518:76 V3 testdata/Builtins.lc 518:39-518:48 'Nat -> Type->Type testdata/Builtins.lc 518:35-518:76 'Nat testdata/Builtins.lc 518:35-518:76 V1 testdata/Builtins.lc 518:51-518:56 Type testdata/Builtins.lc 518:71-518:76 Type testdata/Builtins.lc 518:1-518:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 518:15-518:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 519:35-519:72 Type testdata/Builtins.lc 519:35-519:72 V1 testdata/Builtins.lc 519:39-519:56 Type testdata/Builtins.lc 519:39-519:48 'Nat -> Type->Type testdata/Builtins.lc 519:51-519:56 Type testdata/Builtins.lc 519:1-519:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a testdata/Builtins.lc 520:35-520:67 Type testdata/Builtins.lc 520:35-520:67 V3 testdata/Builtins.lc 520:39-520:48 'Nat -> Type->Type testdata/Builtins.lc 520:35-520:67 'Nat testdata/Builtins.lc 520:35-520:67 V1 testdata/Builtins.lc 520:51-520:56 Type testdata/Builtins.lc 520:1-520:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 521:35-521:77 Type testdata/Builtins.lc 521:35-521:77 V3 testdata/Builtins.lc 521:39-521:48 'Nat -> Type->Type testdata/Builtins.lc 521:35-521:77 'Nat testdata/Builtins.lc 521:35-521:77 V1 testdata/Builtins.lc 521:51-521:56 Type testdata/Builtins.lc 521:1-521:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 521:18-521:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 522:35-522:72 Type testdata/Builtins.lc 522:35-522:72 V3 testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type testdata/Builtins.lc 522:35-522:72 'Nat testdata/Builtins.lc 522:35-522:72 V1 testdata/Builtins.lc 522:51-522:56 Type testdata/Builtins.lc 522:1-522:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 524:34-524:56 Type testdata/Builtins.lc 524:34-524:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 524:34-524:56 'Nat testdata/Builtins.lc 524:34-524:56 V5 testdata/Builtins.lc 524:34-524:56 V3 testdata/Builtins.lc 524:34-524:56 V1 testdata/Builtins.lc 524:47-524:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 524:1-524:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Mat b a c testdata/Builtins.lc 525:34-525:52 Type testdata/Builtins.lc 525:34-525:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 525:34-525:52 'Nat testdata/Builtins.lc 525:34-525:52 V3 testdata/Builtins.lc 525:34-525:52 V1 testdata/Builtins.lc 525:47-525:52 Type testdata/Builtins.lc 525:1-525:16 {a:'Nat} -> {b} -> 'Mat a a b -> 'Float testdata/Builtins.lc 526:34-526:56 Type testdata/Builtins.lc 526:34-526:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 526:34-526:56 'Nat testdata/Builtins.lc 526:34-526:56 V3 testdata/Builtins.lc 526:34-526:56 V1 testdata/Builtins.lc 526:47-526:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 526:1-526:12 {a:'Nat} -> {b} -> 'Mat a a b -> 'Mat a a b testdata/Builtins.lc 527:34-527:69 Type testdata/Builtins.lc 527:34-527:37 'Nat -> Type->Type testdata/Builtins.lc 527:34-527:69 'Nat testdata/Builtins.lc 527:34-527:69 V5 testdata/Builtins.lc 527:34-527:69 V3 testdata/Builtins.lc 527:47-527:50 'Nat -> Type->Type testdata/Builtins.lc 527:34-527:69 V2 testdata/Builtins.lc 527:60-527:63 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 527:1-527:17 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'VecS b c -> 'Mat c a b testdata/Builtins.lc 528:34-528:67 Type testdata/Builtins.lc 528:34-528:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 528:34-528:67 'Nat testdata/Builtins.lc 528:34-528:67 V5 testdata/Builtins.lc 528:34-528:67 V3 testdata/Builtins.lc 528:34-528:67 V1 testdata/Builtins.lc 528:47-528:50 'Nat -> Type->Type testdata/Builtins.lc 528:60-528:63 'Nat -> Type->Type testdata/Builtins.lc 528:1-528:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'VecS c b -> 'VecS c a testdata/Builtins.lc 529:34-529:67 Type testdata/Builtins.lc 529:34-529:37 'Nat -> Type->Type testdata/Builtins.lc 529:34-529:67 'Nat testdata/Builtins.lc 529:34-529:67 V5 testdata/Builtins.lc 529:34-529:67 V3 testdata/Builtins.lc 529:47-529:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 529:34-529:67 V2 testdata/Builtins.lc 529:60-529:63 'Nat -> Type->Type testdata/Builtins.lc 529:1-529:14 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'Mat a c b -> 'VecS b c testdata/Builtins.lc 530:34-530:69 Type testdata/Builtins.lc 530:34-530:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 530:34-530:69 'Nat testdata/Builtins.lc 530:34-530:69 V7 testdata/Builtins.lc 530:34-530:69 V5 testdata/Builtins.lc 530:34-530:69 V3 testdata/Builtins.lc 530:47-530:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 530:34-530:69 V2 testdata/Builtins.lc 530:60-530:63 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 530:1-530:14 {a:'Nat} -> {b:'Nat} -> {c} -> {d:'Nat} -> 'Mat a b c -> 'Mat b d c -> 'Mat a d c testdata/Builtins.lc 533:35-533:97 Type testdata/Builtins.lc 533:35-533:38 Type->Type testdata/Builtins.lc 533:35-533:97 V7 testdata/Builtins.lc 533:35-533:97 V6 testdata/Builtins.lc 533:46-533:55 'Nat -> Type->Type testdata/Builtins.lc 533:35-533:97 'Nat testdata/Builtins.lc 533:35-533:97 V4 testdata/Builtins.lc 533:35-533:97 V3 testdata/Builtins.lc 533:65-533:74 'Nat -> Type->Type testdata/Builtins.lc 533:77-533:81 Type testdata/Builtins.lc 532:1-532: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 532:15-532: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 532:34-532: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 532:51-532: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 532:73-532: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 532:85-532: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 534:35-534:76 Type testdata/Builtins.lc 534:35-534:76 V3 testdata/Builtins.lc 534:39-534:55 Type->Type testdata/Builtins.lc 534:35-534:76 V1 testdata/Builtins.lc 534:72-534:76 Type testdata/Builtins.lc 534:1-534:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 534:12-534:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 537:35-537:67 Type testdata/Builtins.lc 537:35-537:67 V3 testdata/Builtins.lc 537:39-537:48 'Nat -> Type->Type testdata/Builtins.lc 537:35-537:67 'Nat testdata/Builtins.lc 537:35-537:67 V1 testdata/Builtins.lc 537:51-537:56 Type testdata/Builtins.lc 536:1-536:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 536:11-536:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 536:21-536:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 539:34-539:60 Type testdata/Builtins.lc 539:34-539:43 'Nat -> Type->Type testdata/Builtins.lc 539:34-539:60 'Nat testdata/Builtins.lc 539:34-539:60 V1 testdata/Builtins.lc 539:46-539:51 Type testdata/Builtins.lc 539:55-539:60 Type testdata/Builtins.lc 539:1-539:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float testdata/Builtins.lc 540:34-540:66 Type testdata/Builtins.lc 540:34-540:43 'Nat -> Type->Type testdata/Builtins.lc 540:34-540:66 'Nat testdata/Builtins.lc 540:34-540:66 V1 testdata/Builtins.lc 540:46-540:51 Type testdata/Builtins.lc 540:55-540:66 Type testdata/Builtins.lc 540:55-540:58 'Nat -> Type->Type testdata/Builtins.lc 540:61-540:66 Type testdata/Builtins.lc 540:1-540:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 541:34-541:66 Type testdata/Builtins.lc 541:34-541:43 'Nat -> Type->Type testdata/Builtins.lc 541:34-541:66 'Nat testdata/Builtins.lc 541:34-541:66 V1 testdata/Builtins.lc 541:46-541:51 Type testdata/Builtins.lc 541:55-541:66 Type testdata/Builtins.lc 541:55-541:58 'Nat -> Type->Type testdata/Builtins.lc 541:61-541:66 Type testdata/Builtins.lc 541:1-541:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 542:34-542:66 Type testdata/Builtins.lc 542:34-542:43 'Nat -> Type->Type testdata/Builtins.lc 542:34-542:66 'Nat testdata/Builtins.lc 542:34-542:66 V1 testdata/Builtins.lc 542:46-542:51 Type testdata/Builtins.lc 542:55-542:66 Type testdata/Builtins.lc 542:55-542:58 'Nat -> Type->Type testdata/Builtins.lc 542:61-542:66 Type testdata/Builtins.lc 542:1-542:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 558:6-558:13 Type testdata/Builtins.lc 559:20-559:26 Type testdata/Builtins.lc 560:20-560:27 Type testdata/Builtins.lc 559:3-559:16 'String->'Texture testdata/Builtins.lc 562:20-562:23 'Nat -> Type->Type testdata/Builtins.lc 562:26-562:29 Type testdata/Builtins.lc 563:20-564:27 Type testdata/Builtins.lc 563:20-563:25 'Nat -> Type->Type testdata/Builtins.lc 563:29-563:47 Type testdata/Builtins.lc 563:29-563:34 Type->Type testdata/Builtins.lc 563:36-563:47 Type testdata/Builtins.lc 563:36-563:39 'Nat -> Type->Type testdata/Builtins.lc 563:42-563:47 Type testdata/Builtins.lc 564:20-564:27 Type testdata/Builtins.lc 562:3-562:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture testdata/Builtins.lc 566:6-566:12 Type testdata/Builtins.lc 567:5-567:16 'Filter testdata/Builtins.lc 568:5-568:17 'Filter testdata/Builtins.lc 570:6-570:14 Type testdata/Builtins.lc 571:5-571:11 'EdgeMode testdata/Builtins.lc 572:5-572:19 'EdgeMode testdata/Builtins.lc 573:5-573:16 'EdgeMode testdata/Builtins.lc 575:6-575:13 Type testdata/Builtins.lc 575:24-575:30 Type testdata/Builtins.lc 575:6-575:47 Type testdata/Builtins.lc 575:31-575:39 Type testdata/Builtins.lc 575:40-575:47 Type testdata/Builtins.lc 575:16-575:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler testdata/Builtins.lc 578:14-578:21 Type testdata/Builtins.lc 578:25-578:51 Type testdata/Builtins.lc 578:25-578:28 'Nat -> Type->Type testdata/Builtins.lc 578:31-578:36 Type testdata/Builtins.lc 578:40-578:51 Type testdata/Builtins.lc 578:40-578:43 'Nat -> Type->Type testdata/Builtins.lc 578:46-578:51 Type testdata/Builtins.lc 578:1-578:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 581:30-581:39 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 581:41-581:60 V1->V1 testdata/Builtins.lc 581:41-581: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 581:53-581:60 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float testdata/Builtins.lc 581:59-581:60 'Float testdata/Builtins.lc 581:59-581:60 'Int testdata/Builtins.lc 581:1-581: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 582:46-582:55 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 582:57-582:67 V1->V1 testdata/Builtins.lc 582:57-582: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 582:1-582: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 583:24-583:32 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 583:1-583:15 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 584:25-584:35 V2 -> V2->V2 testdata/Builtins.lc 584:25-584:35 V2->V2 testdata/Builtins.lc 584:25-584:35 V2 testdata/Builtins.lc 584:25-584:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 584:13-584:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) testdata/Builtins.lc 584:13-584:21 V4 testdata/Builtins.lc 584:1-584:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b testdata/Builtins.lc 585:15-585:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 585:1-585:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 586:14-586:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 586:1-586:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 587:19-587:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 587:1-587:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) testdata/Builtins.lc 588:19-588:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 588:1-588:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c)