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 Type->Type testdata/Builtins.lc 26:10-26:24 Type testdata/Builtins.lc 25:7-25:21 Type->Type testdata/Builtins.lc 28:10-28:21 Type->Type testdata/Builtins.lc 28:10-28:21 Type testdata/Builtins.lc 27:7-27:18 Type->Type testdata/Builtins.lc 30:10-30:26 Type->Type testdata/Builtins.lc 30:10-30:26 Type testdata/Builtins.lc 29:7-29:23 Type->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 Type->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 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 Type->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 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 Type->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 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 Type->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 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:21-357:59 Type testdata/Builtins.lc 357:21-357:59 V3 testdata/Builtins.lc 357:26-357:32 Type->Type testdata/Builtins.lc 357:21-357:59 V2 testdata/Builtins.lc 357:39-357:45 Type->Type testdata/Builtins.lc 357:51-357:57 Type->Type testdata/Builtins.lc 357:1-357:16 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b testdata/Builtins.lc 358:18-358:52 Type testdata/Builtins.lc 358:18-358:52 V1 testdata/Builtins.lc 358:23-358:27 Type testdata/Builtins.lc 358:32-358:38 Type->Type testdata/Builtins.lc 358:44-358:50 Type->Type testdata/Builtins.lc 358:1-358:13 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 360:22-360:35 Type testdata/Builtins.lc 360:6-360:15 'PrimitiveType -> Type->Type testdata/Builtins.lc 362:28-362:34 Type->Type testdata/Builtins.lc 362:36-362:49 Type testdata/Builtins.lc 362:36-362:45 'PrimitiveType -> Type->Type testdata/Builtins.lc 362:46-362:47 'PrimitiveType testdata/Builtins.lc 362:46-362:47 V3 testdata/Builtins.lc 362:48-362:49 Type testdata/Builtins.lc 362:48-362:49 V1 testdata/Builtins.lc 362:6-362:21 'PrimitiveType -> Type->Type testdata/Builtins.lc 364:18-364:59 Type testdata/Builtins.lc 364:18-364:59 V5 testdata/Builtins.lc 364:18-364:59 V4 testdata/Builtins.lc 364:29-364:38 'PrimitiveType -> Type->Type testdata/Builtins.lc 364:18-364:59 'PrimitiveType testdata/Builtins.lc 364:18-364:59 V2 testdata/Builtins.lc 364:46-364:55 'PrimitiveType -> Type->Type testdata/Builtins.lc 364:1-364:13 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 366:39-366:94 Type testdata/Builtins.lc 366:39-366:53 Type->Type testdata/Builtins.lc 366:54-366:55 Type testdata/Builtins.lc 366:54-366:55 V1 testdata/Builtins.lc 366:60-366:94 Type testdata/Builtins.lc 366:60-366:66 Type testdata/Builtins.lc 366:70-366:94 Type testdata/Builtins.lc 366:70-366:71 Type testdata/Builtins.lc 366:75-366:94 Type testdata/Builtins.lc 366:75-366:90 'PrimitiveType -> Type->Type testdata/Builtins.lc 366:91-366:92 'PrimitiveType testdata/Builtins.lc 366:91-366:92 V5 testdata/Builtins.lc 366:93-366:94 Type testdata/Builtins.lc 366:1-366:7 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 367:42-367:104 Type testdata/Builtins.lc 367:42-367:56 Type->Type testdata/Builtins.lc 367:57-367:58 Type testdata/Builtins.lc 367:57-367:58 V3 testdata/Builtins.lc 367:60-367:104 Type testdata/Builtins.lc 367:60-367:61 Type testdata/Builtins.lc 367:64-367:74 Type testdata/Builtins.lc 367:64-367:71 Type->Type testdata/Builtins.lc 367:72-367:74 Type testdata/Builtins.lc 367:72-367:74 V2 testdata/Builtins.lc 367:79-367:104 Type testdata/Builtins.lc 367:79-367:81 Type testdata/Builtins.lc 367:85-367:104 Type testdata/Builtins.lc 367:85-367:100 'PrimitiveType -> Type->Type testdata/Builtins.lc 367:101-367:102 'PrimitiveType testdata/Builtins.lc 367:101-367:102 V6 testdata/Builtins.lc 367:103-367:104 Type testdata/Builtins.lc 367:1-367:13 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 369:19-369:74 Type testdata/Builtins.lc 369:19-369:74 V5 testdata/Builtins.lc 369:19-369:74 V4 testdata/Builtins.lc 369:31-369:46 'PrimitiveType -> Type->Type testdata/Builtins.lc 369:19-369:74 'PrimitiveType testdata/Builtins.lc 369:19-369:74 V2 testdata/Builtins.lc 369:55-369:70 'PrimitiveType -> Type->Type testdata/Builtins.lc 370:19-370:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 370:19-370:42 {a} -> {b:'PrimitiveType} -> V2->a -> 'Stream ('Primitive b V3) -> 'Stream ('Primitive b a) testdata/Builtins.lc 370:19-370:42 {a:'PrimitiveType} -> V2->V2 -> 'Stream ('Primitive a V3) -> 'Stream ('Primitive a V3) testdata/Builtins.lc 370:19-370:42 V2->V2 -> 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 370:19-370:42 'Stream ('Primitive V1 V3) -> 'Stream ('Primitive V2 V3) testdata/Builtins.lc 370:19-370:28 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 370:30-370:42 V1->V1 testdata/Builtins.lc 370:30-370:42 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive c a -> 'Primitive c b testdata/Builtins.lc 370:1-370:14 {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Stream ('Primitive c a) -> 'Stream ('Primitive c b) testdata/Builtins.lc 372:15-372:21 {a:'PrimitiveType} -> {b} -> {c:'Unit} -> 'String -> b -> 'Stream ('Primitive a b) testdata/Builtins.lc 372:1-372:6 {a} -> 'String -> c:'PrimitiveType -> a -> 'Stream ('Primitive c a) testdata/Builtins.lc 373:19-373:31 {a:'PrimitiveType} -> {b} -> {c} -> {d:'Unit} -> {e : b ~ 'FTRepr' c} -> c -> 'Stream ('Primitive a b) testdata/Builtins.lc 373:1-373:12 {a} -> b:'PrimitiveType -> a -> 'Stream ('Primitive b ('FTRepr' a)) testdata/Builtins.lc 375:6-375:18 Type testdata/Builtins.lc 375:21-375:28 'DepthHandler testdata/Builtins.lc 375:31-375:43 'DepthHandler testdata/Builtins.lc 392:23-402:82 Type->Type testdata/Builtins.lc 392:23-402:82 Type testdata/Builtins.lc 392:23-392:25 Type testdata/Builtins.lc 393:25-402:82 Type testdata/Builtins.lc 393:25-393:26 Type testdata/Builtins.lc 394:19-402:82 Type testdata/Builtins.lc 394:39-394:45 Type -> Type->Type testdata/Builtins.lc 394:39-394:45 Type->Type testdata/Builtins.lc 394:39-394:45 Type testdata/Builtins.lc 394:19-394:35 Type testdata/Builtins.lc 395:19-402:82 Type testdata/Builtins.lc 395:48-400:58 Type -> Type -> Type->Type testdata/Builtins.lc 395:48-400:58 Type -> Type->Type testdata/Builtins.lc 395:48-400:58 Type->Type testdata/Builtins.lc 395:48-400:58 Type testdata/Builtins.lc 395:48-395:57 Type->Type testdata/Builtins.lc 395:48-395:57 Type testdata/Builtins.lc 395:48-395:57 Type -> Type -> Type->Type testdata/Builtins.lc 400:52-400:58 Type testdata/Builtins.lc 400:52-400:58 Type->Type testdata/Builtins.lc 400:52-400:58 Type -> Type->Type testdata/Builtins.lc 395:19-395:44 Type testdata/Builtins.lc 396:19-402:82 Type testdata/Builtins.lc 396:57-401:70 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 396:57-401:70 Type -> Type -> Type->Type testdata/Builtins.lc 396:57-401:70 Type -> Type->Type testdata/Builtins.lc 396:57-401:70 Type->Type testdata/Builtins.lc 396:57-401:70 Type testdata/Builtins.lc 396:57-396:69 Type->Type testdata/Builtins.lc 396:57-396:69 Type testdata/Builtins.lc 396:57-396:69 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 401:61-401:70 Type testdata/Builtins.lc 401:61-401:70 Type->Type testdata/Builtins.lc 401:61-401:70 Type -> Type -> Type->Type testdata/Builtins.lc 396:19-396:53 Type testdata/Builtins.lc 397:19-402:82 Type testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 397:66-402:82 Type -> Type -> Type->Type testdata/Builtins.lc 397:66-402:82 Type -> Type->Type testdata/Builtins.lc 397:66-402:82 Type->Type testdata/Builtins.lc 397:66-402:82 Type testdata/Builtins.lc 397:66-397:81 Type->Type testdata/Builtins.lc 397:66-397:81 Type testdata/Builtins.lc 397:66-397:81 Type -> Type -> Type -> Type -> Type->Type testdata/Builtins.lc 402:70-402:82 Type testdata/Builtins.lc 402:70-402:82 Type->Type testdata/Builtins.lc 402:70-402:82 Type -> Type -> Type -> Type->Type testdata/Builtins.lc 397:19-397:62 Type testdata/Builtins.lc 398:25-398:36 Type testdata/Builtins.lc 398:34-398:36 Type->Type testdata/Builtins.lc 398:34-398:36 Type testdata/Builtins.lc 398:25-398:30 Type testdata/Builtins.lc 392:5-392:17 Type->Type testdata/Builtins.lc 406:18-406:21 Type testdata/Builtins.lc 406:25-406:53 Type testdata/Builtins.lc 406:25-406:37 Type testdata/Builtins.lc 406:41-406:53 Type testdata/Builtins.lc 406:41-406:45 Type testdata/Builtins.lc 406:49-406:53 Type testdata/Builtins.lc 406:6-406:14 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 408:29-408:35 Type->Type testdata/Builtins.lc 408:37-408:51 Type testdata/Builtins.lc 408:37-408:45 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 408:46-408:47 'Nat testdata/Builtins.lc 408:46-408:47 V5 testdata/Builtins.lc 408:48-408:49 'DepthHandler testdata/Builtins.lc 408:48-408:49 V3 testdata/Builtins.lc 408:50-408:51 Type testdata/Builtins.lc 408:50-408:51 V1 testdata/Builtins.lc 408:6-408:20 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 410:20-410:78 Type testdata/Builtins.lc 410:20-410:78 V3 testdata/Builtins.lc 410:25-410:30 Type testdata/Builtins.lc 410:35-410:43 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 410:20-410:78 'Nat testdata/Builtins.lc 410:20-410:78 V2 testdata/Builtins.lc 410:53-410:61 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 410:64-410:76 'DepthHandler testdata/Builtins.lc 410:1-410:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 412:21-412:30 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 412:32-412:46 V1->V1 testdata/Builtins.lc 412:32-412:46 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Fragment c a b -> 'Fragment c DefinedDepth b testdata/Builtins.lc 412:1-412:16 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Float -> 'Stream ('Fragment c a b) -> 'Stream ('Fragment c DefinedDepth b) testdata/Builtins.lc 419:21-423:68 Type testdata/Builtins.lc 419:21-423:68 V7 testdata/Builtins.lc 419:25-419:41 Type->Type testdata/Builtins.lc 419:21-423:68 V5 testdata/Builtins.lc 419:21-423:68 V4 testdata/Builtins.lc 419:49-419:62 Type -> Type->Type testdata/Builtins.lc 419:64-419:75 Type testdata/Builtins.lc 419:64-419:67 'Nat -> Type->Type testdata/Builtins.lc 419:70-419:75 Type testdata/Builtins.lc 420:26-420:31 Type testdata/Builtins.lc 422:20-422:33 'PrimitiveType->Type testdata/Builtins.lc 419:21-423:68 'PrimitiveType testdata/Builtins.lc 423:20-423:29 'PrimitiveType -> Type->Type testdata/Builtins.lc 423:37-423:51 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 423:54-423:66 'DepthHandler testdata/Builtins.lc 419:1-419:11 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) testdata/Builtins.lc 425:20-425:56 Type testdata/Builtins.lc 425:20-425:56 V3 testdata/Builtins.lc 425:25-425:29 Type testdata/Builtins.lc 425:34-425:42 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 425:20-425:56 'Nat testdata/Builtins.lc 425:20-425:56 V2 testdata/Builtins.lc 425:52-425:56 Type testdata/Builtins.lc 425:1-425:15 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 427:21-427:82 Type testdata/Builtins.lc 427:21-427:82 V5 testdata/Builtins.lc 427:26-427:30 Type testdata/Builtins.lc 427:36-427:50 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 427:21-427:82 'Nat testdata/Builtins.lc 427:21-427:82 V4 testdata/Builtins.lc 427:21-427:82 'DepthHandler testdata/Builtins.lc 427:21-427:82 V2 testdata/Builtins.lc 427:62-427:76 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 428:21-428:49 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 428:21-428:49 {a:'Nat} -> {b:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment a b V3) -> 'Stream ('Fragment a b V4) testdata/Builtins.lc 428:21-428:49 {a:'DepthHandler} -> V2->'Bool -> 'Stream ('Fragment V2 a V3) -> 'Stream ('Fragment V3 a V4) testdata/Builtins.lc 428:21-428:49 V2->'Bool -> 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 428:21-428:49 'Stream ('Fragment V2 V1 V3) -> 'Stream ('Fragment V3 V2 V4) testdata/Builtins.lc 428:21-428:33 {a} -> a->'Bool -> 'Stream a -> 'Stream a testdata/Builtins.lc 428:35-428:49 V0->'Bool testdata/Builtins.lc 428:35-428:49 {a:'DepthHandler} -> {b} -> {c:'Nat} -> b->'Bool -> 'Fragment c a b -> 'Bool testdata/Builtins.lc 428:1-428:16 {a} -> {b:'Nat} -> {c:'DepthHandler} -> a->'Bool -> 'Stream ('Fragment b c a) -> 'Stream ('Fragment b c a) testdata/Builtins.lc 430:17-430:60 Type testdata/Builtins.lc 430:17-430:60 V7 testdata/Builtins.lc 430:17-430:60 V6 testdata/Builtins.lc 430:28-430:36 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 430:17-430:60 'Nat testdata/Builtins.lc 430:17-430:60 V4 testdata/Builtins.lc 430:17-430:60 'DepthHandler testdata/Builtins.lc 430:17-430:60 V2 testdata/Builtins.lc 430:46-430:54 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 430:1-430:12 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 432:18-432:27 {a} -> {b} -> a->b -> 'Stream a -> 'Stream b testdata/Builtins.lc 432:29-432:40 V1->V1 testdata/Builtins.lc 432:29-432:40 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Fragment c d a -> 'Fragment c d b testdata/Builtins.lc 432:1-432:13 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 437:13-437:26 Type->Type testdata/Builtins.lc 442:13-442:28 Type->Type testdata/Builtins.lc 445:10-446:36 Type->Type testdata/Builtins.lc 445:10-446:36 Type testdata/Builtins.lc 445:10-445:23 Type->Type testdata/Builtins.lc 445:10-445:23 Type testdata/Builtins.lc 445:10-445:23 Type -> 'Nat->Type testdata/Builtins.lc 445:10-445:23 'Nat->Type testdata/Builtins.lc 445:37-445:44 Type testdata/Builtins.lc 446:10-446:36 Type testdata/Builtins.lc 446:10-446:23 Type->Type testdata/Builtins.lc 446:10-446:23 Type testdata/Builtins.lc 446:31-446:36 Type testdata/Builtins.lc 444:7-444:20 Type->Type testdata/Builtins.lc 444:7-444:65 Type testdata/Builtins.lc 444:46-444:65 Type testdata/Builtins.lc 444:46-444:63 Type->Type testdata/Builtins.lc 444:64-444:65 Type testdata/Builtins.lc 445:37-446:77 {a} -> {b : 'DefaultFragOp a} -> 'FragmentOperation a testdata/Builtins.lc 445:37-446:77 {a : 'DefaultFragOp V0} -> 'FragmentOperation V1 testdata/Builtins.lc 445:69-445:111 a:Type -> {b : 'DefaultFragOp ('Color a)} -> 'FragmentOperation ('Color a) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color V0)} -> 'FragmentOperation ('Color V1) testdata/Builtins.lc 445:69-445:111 a:Type -> b:'Nat -> {c : 'DefaultFragOp ('Color ('VecS a b))} -> 'FragmentOperation ('Color ('VecS a b)) testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS V1 a))} -> 'FragmentOperation ('Color ('VecS V2 a)) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS V1 V0))} -> 'FragmentOperation ('Color ('VecS V2 V1)) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float V0))} -> 'FragmentOperation ('Color ('VecS 'Float V1)) testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ a)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ a))) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ V0)))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ V1))) testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ a))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ a)))) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ V0))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ V1)))) testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ a)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ a))))) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ V0)))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ V1))))) testdata/Builtins.lc 445:69-445:111 a:'Nat -> {b : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ a)))))) testdata/Builtins.lc 445:69-445:111 {a : 'DefaultFragOp ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V0))))))} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ V1)))))) testdata/Builtins.lc 445:69-445:111 {a:'Unit} -> 'FragmentOperation ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) testdata/Builtins.lc 445:69-445:76 {a} -> {b:'Nat} -> {c} -> {d} -> {e : a ~ 'VecScalar b 'Bool} -> {f : c ~ 'VecScalar b d} -> {g : 'Num d} -> 'Blending d -> a -> 'FragmentOperation ('Color c) testdata/Builtins.lc 445:77-445:87 'Blending V1 testdata/Builtins.lc 445:77-445:87 {a} -> 'Blending a testdata/Builtins.lc 445:89-445:111 'VecScalar V2 'Bool testdata/Builtins.lc 445:89-445:91 {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 445:92-445:96 V0 testdata/Builtins.lc 445:92-445:96 'Bool testdata/Builtins.lc 445:97-445:101 'Bool testdata/Builtins.lc 445:102-445:106 'Bool testdata/Builtins.lc 445:107-445:111 'Bool testdata/Builtins.lc 446:31-446:77 {a : 'DefaultFragOp V1} -> 'FragmentOperation V2 testdata/Builtins.lc 446:60-446:77 a:Type -> {b : 'DefaultFragOp ('Depth a)} -> 'FragmentOperation ('Depth a) testdata/Builtins.lc 446:60-446:77 {a : 'DefaultFragOp ('Depth V0)} -> 'FragmentOperation ('Depth V1) testdata/Builtins.lc 446:60-446:77 {a:'Unit} -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 446:60-446:67 'ComparisonFunction -> 'Bool -> 'FragmentOperation ('Depth 'Float) testdata/Builtins.lc 446:68-446:72 'ComparisonFunction testdata/Builtins.lc 446:73-446:77 'Bool testdata/Builtins.lc 444:29-444:42 {a} -> {b} -> {c : 'DefaultFragOp b} -> 'FragmentOperation b testdata/Builtins.lc 453:24-453:27 Type testdata/Builtins.lc 453:6-453:17 'Nat -> Type->Type testdata/Builtins.lc 454:19-454:108 Type testdata/Builtins.lc 454:19-454:27 Type->Type testdata/Builtins.lc 454:28-454:29 Type testdata/Builtins.lc 454:34-454:48 'Nat -> 'DepthHandler -> Type->Type testdata/Builtins.lc 454:49-454:50 'Nat testdata/Builtins.lc 454:19-454:108 'DepthHandler testdata/Builtins.lc 454:19-454:108 V2 testdata/Builtins.lc 454:54-454:68 Type testdata/Builtins.lc 454:54-454:66 Type->Type testdata/Builtins.lc 454:67-454:68 Type testdata/Builtins.lc 454:74-454:108 Type testdata/Builtins.lc 454:74-454:85 'Nat -> Type->Type testdata/Builtins.lc 454:86-454:87 'Nat testdata/Builtins.lc 454:88-454:89 Type testdata/Builtins.lc 454:93-454:108 Type testdata/Builtins.lc 454:93-454:104 'Nat -> Type->Type testdata/Builtins.lc 454:105-454:106 'Nat testdata/Builtins.lc 454:107-454:108 Type testdata/Builtins.lc 454:3-454:13 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 455:20-455:117 Type testdata/Builtins.lc 455:20-455:36 Type->Type testdata/Builtins.lc 455:37-455:38 Type testdata/Builtins.lc 455:40-455:55 Type->Type testdata/Builtins.lc 455:20-455:117 V2 testdata/Builtins.lc 455:59-455:74 Type testdata/Builtins.lc 455:59-455:70 'Nat -> Type->Type testdata/Builtins.lc 455:71-455:72 'Nat testdata/Builtins.lc 455:73-455:74 Type testdata/Builtins.lc 455:77-455:90 Type->Type testdata/Builtins.lc 455:102-455:117 Type testdata/Builtins.lc 455:102-455:113 'Nat -> Type->Type testdata/Builtins.lc 455:114-455:115 'Nat testdata/Builtins.lc 455:116-455:117 Type testdata/Builtins.lc 455:3-455:14 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 457:34-457:44 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 457:50-457:62 'Stream ('Fragment V2 V0 ('RemSemantics V1)) testdata/Builtins.lc 457:50-457:62 {a} -> {b} -> {c:'Nat} -> {d:'DepthHandler} -> a->b -> 'Stream ('Fragment c d a) -> 'Stream ('Fragment c d b) testdata/Builtins.lc 457:1-457:11 {a:'Nat} -> {b} -> {c:'DepthHandler} -> {d} -> 'FragOps' b -> (d -> 'RemSemantics b) -> 'Stream ('Fragment a c d) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 459:1-459:20 {a} -> a->a testdata/Builtins.lc 461:15-461:18 Type testdata/Builtins.lc 461:22-461:34 Type testdata/Builtins.lc 461:22-461:26 Type testdata/Builtins.lc 461:30-461:34 Type testdata/Builtins.lc 461:6-461:11 'Nat -> Type->Type testdata/Builtins.lc 462:48-463:56 Type testdata/Builtins.lc 462:48-462:51 Type->Type testdata/Builtins.lc 462:52-462:53 Type testdata/Builtins.lc 462:52-462:53 V3 testdata/Builtins.lc 462:55-463:56 Type testdata/Builtins.lc 462:55-462:60 Type testdata/Builtins.lc 462:55-462:60 V2 testdata/Builtins.lc 462:63-462:76 Type testdata/Builtins.lc 462:63-462:72 'Nat -> Type->Type testdata/Builtins.lc 462:73-462:74 'Nat testdata/Builtins.lc 462:73-462:74 V4 testdata/Builtins.lc 462:75-462:76 Type testdata/Builtins.lc 463:26-463:56 Type testdata/Builtins.lc 463:26-463:31 Type testdata/Builtins.lc 463:36-463:56 Type testdata/Builtins.lc 463:36-463:41 'Nat -> Type->Type testdata/Builtins.lc 463:42-463:43 'Nat testdata/Builtins.lc 463:42-463:43 V7 testdata/Builtins.lc 463:45-463:56 Type testdata/Builtins.lc 463:45-463:50 Type->Type testdata/Builtins.lc 463:51-463:56 Type testdata/Builtins.lc 462:3-462:13 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 464:37-464:67 Type testdata/Builtins.lc 464:37-464:42 Type testdata/Builtins.lc 464:47-464:67 Type testdata/Builtins.lc 464:47-464:52 'Nat -> Type->Type testdata/Builtins.lc 464:53-464:54 'Nat testdata/Builtins.lc 464:53-464:54 V2 testdata/Builtins.lc 464:56-464:67 Type testdata/Builtins.lc 464:56-464:61 Type->Type testdata/Builtins.lc 464:62-464:67 Type testdata/Builtins.lc 464:3-464:13 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 465:37-465:67 Type testdata/Builtins.lc 465:37-465:40 Type testdata/Builtins.lc 465:47-465:67 Type testdata/Builtins.lc 465:47-465:52 'Nat -> Type->Type testdata/Builtins.lc 465:53-465:54 'Nat testdata/Builtins.lc 465:53-465:54 V2 testdata/Builtins.lc 465:56-465:67 Type testdata/Builtins.lc 465:56-465:63 Type->Type testdata/Builtins.lc 465:64-465:67 Type testdata/Builtins.lc 465:3-465:15 {a:'Nat} -> 'Int -> 'Image a ('Stencil 'Int) testdata/Builtins.lc 468:26-468:54 Type testdata/Builtins.lc 468:26-468:37 'Nat -> Type->Type testdata/Builtins.lc 468:26-468:54 V1 testdata/Builtins.lc 468:45-468:50 'Nat -> Type->Type testdata/Builtins.lc 468:3-468:11 {a} -> 'FrameBuffer (Succ Zero) a -> 'Image (Succ Zero) a testdata/Builtins.lc 469:26-469:37 'Nat -> Type->Type testdata/Builtins.lc 469:40-469:74 Type testdata/Builtins.lc 469:40-469:74 Type -> Type->Type testdata/Builtins.lc 469:41-469:52 Type testdata/Builtins.lc 469:41-469:46 Type->Type testdata/Builtins.lc 469:47-469:52 Type testdata/Builtins.lc 469:54-469:72 Type testdata/Builtins.lc 469:54-469:59 Type->Type testdata/Builtins.lc 469:61-469:72 Type testdata/Builtins.lc 469:61-469:64 'Nat -> Type->Type testdata/Builtins.lc 469:67-469:72 Type testdata/Builtins.lc 469:78-469:105 Type testdata/Builtins.lc 469:78-469:83 'Nat -> Type->Type testdata/Builtins.lc 469:87-469:105 Type testdata/Builtins.lc 469:87-469:92 Type->Type testdata/Builtins.lc 469:94-469:105 Type testdata/Builtins.lc 469:94-469:97 'Nat -> Type->Type testdata/Builtins.lc 469:100-469:105 Type testdata/Builtins.lc 469:3-469:16 'FrameBuffer (Succ Zero) ('Tuple2 ('Depth 'Float) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) testdata/Builtins.lc 463:42-469:105 Type testdata/Builtins.lc 463:42-463:56 Type testdata/Builtins.lc 464:53-469:105 Type testdata/Builtins.lc 464:53-464:67 Type testdata/Builtins.lc 465:53-469:105 Type testdata/Builtins.lc 465:53-465:67 Type testdata/Builtins.lc 468:26-469:105 Type testdata/Builtins.lc 471:6-471:12 Type testdata/Builtins.lc 472:26-472:51 Type testdata/Builtins.lc 472:26-472:37 'Nat -> Type->Type testdata/Builtins.lc 472:26-472:51 'Nat testdata/Builtins.lc 472:26-472:51 V3 testdata/Builtins.lc 472:26-472:51 V1 testdata/Builtins.lc 472:45-472:51 Type testdata/Builtins.lc 472:3-472:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 478:34-478:73 Type testdata/Builtins.lc 478:34-478:37 Type->Type testdata/Builtins.lc 478:39-478:55 Type->Type testdata/Builtins.lc 478:34-478:73 V1 testdata/Builtins.lc 478:1-478:8 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 478:10-478:17 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 478:19-478:26 {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a testdata/Builtins.lc 479:35-479:80 Type testdata/Builtins.lc 479:35-479:80 V3 testdata/Builtins.lc 479:39-479:55 Type->Type testdata/Builtins.lc 479:35-479:80 V1 testdata/Builtins.lc 479:59-479:62 Type->Type testdata/Builtins.lc 479:1-479:9 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 479:11-479:19 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 479:21-479:29 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b testdata/Builtins.lc 480:35-480:75 Type testdata/Builtins.lc 480:35-480:38 Type->Type testdata/Builtins.lc 480:35-480:75 V5 testdata/Builtins.lc 480:35-480:75 V4 testdata/Builtins.lc 480:46-480:55 'Nat -> Type->Type testdata/Builtins.lc 480:35-480:75 'Nat testdata/Builtins.lc 480:35-480:75 V2 testdata/Builtins.lc 480:1-480:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 480:10-480:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 481:35-481:75 Type testdata/Builtins.lc 481:35-481:38 Type->Type testdata/Builtins.lc 481:35-481:75 V5 testdata/Builtins.lc 481:35-481:75 V4 testdata/Builtins.lc 481:46-481:55 '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 : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 481:11-481:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 482:34-482:71 Type testdata/Builtins.lc 482:34-482:40 Type->Type testdata/Builtins.lc 482:42-482:58 Type->Type testdata/Builtins.lc 482:34-482:71 V1 testdata/Builtins.lc 482:1-482:8 {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a testdata/Builtins.lc 484:35-484:80 Type testdata/Builtins.lc 484:35-484:43 Type->Type testdata/Builtins.lc 484:35-484:80 V5 testdata/Builtins.lc 484:35-484:80 V4 testdata/Builtins.lc 484:51-484:60 'Nat -> Type->Type testdata/Builtins.lc 484:35-484:80 'Nat testdata/Builtins.lc 484:35-484:80 V2 testdata/Builtins.lc 484:1-484:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 484:11-484:18 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 484:20-484:28 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 485:35-485:80 Type testdata/Builtins.lc 485:35-485:43 Type->Type testdata/Builtins.lc 485:35-485:80 V5 testdata/Builtins.lc 485:35-485:80 V4 testdata/Builtins.lc 485:51-485:60 'Nat -> Type->Type testdata/Builtins.lc 485:35-485:80 'Nat testdata/Builtins.lc 485:35-485:80 V2 testdata/Builtins.lc 485:1-485:10 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 485:12-485:20 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 485:22-485:31 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 486:35-486:75 Type testdata/Builtins.lc 486:35-486:43 Type->Type testdata/Builtins.lc 486:35-486:75 V5 testdata/Builtins.lc 486:35-486:75 V4 testdata/Builtins.lc 486:51-486:60 'Nat -> Type->Type testdata/Builtins.lc 486:35-486:75 'Nat testdata/Builtins.lc 486:35-486:75 V2 testdata/Builtins.lc 486:1-486:9 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 487:35-487:102 Type testdata/Builtins.lc 487:35-487:43 Type->Type testdata/Builtins.lc 487:35-487:102 V7 testdata/Builtins.lc 487:35-487:102 V6 testdata/Builtins.lc 487:51-487:60 'Nat -> Type->Type testdata/Builtins.lc 487:35-487:102 'Nat testdata/Builtins.lc 487:35-487:102 V4 testdata/Builtins.lc 487:35-487:102 V3 testdata/Builtins.lc 487:70-487:79 'Nat -> Type->Type testdata/Builtins.lc 487:82-487:86 Type testdata/Builtins.lc 487:1-487:12 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b testdata/Builtins.lc 487:14-487:25 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b testdata/Builtins.lc 488:35-488:83 Type testdata/Builtins.lc 488:35-488:43 Type->Type testdata/Builtins.lc 488:35-488:83 V5 testdata/Builtins.lc 488:35-488:83 V4 testdata/Builtins.lc 488:51-488:60 'Nat -> Type->Type testdata/Builtins.lc 488:35-488:83 'Nat testdata/Builtins.lc 488:35-488:83 V2 testdata/Builtins.lc 488:74-488:78 Type testdata/Builtins.lc 488:1-488:13 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 488:15-488:27 {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b testdata/Builtins.lc 490:34-490:38 Type testdata/Builtins.lc 490:42-490:54 Type testdata/Builtins.lc 490:42-490:46 Type testdata/Builtins.lc 490:50-490:54 Type testdata/Builtins.lc 490:1-490:8 'Bool -> 'Bool->'Bool testdata/Builtins.lc 490:10-490:16 'Bool -> 'Bool->'Bool testdata/Builtins.lc 490:18-490:25 'Bool -> 'Bool->'Bool testdata/Builtins.lc 491:35-491:66 Type testdata/Builtins.lc 491:35-491:66 V3 testdata/Builtins.lc 491:39-491:48 'Nat -> Type->Type testdata/Builtins.lc 491:35-491:66 'Nat testdata/Builtins.lc 491:35-491:66 V1 testdata/Builtins.lc 491:51-491:55 Type testdata/Builtins.lc 491:1-491:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a testdata/Builtins.lc 492:34-492:58 Type testdata/Builtins.lc 492:34-492:43 'Nat -> Type->Type testdata/Builtins.lc 492:34-492:58 'Nat testdata/Builtins.lc 492:34-492:58 V1 testdata/Builtins.lc 492:46-492:50 Type testdata/Builtins.lc 492:54-492:58 Type testdata/Builtins.lc 492:1-492:8 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 492:10-492:17 {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool testdata/Builtins.lc 496:35-496:67 Type testdata/Builtins.lc 496:35-496:67 V3 testdata/Builtins.lc 496:39-496:48 'Nat -> Type->Type testdata/Builtins.lc 496:35-496:67 'Nat testdata/Builtins.lc 496:35-496:67 V1 testdata/Builtins.lc 496:51-496:56 Type testdata/Builtins.lc 495:1-495:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:11-495:20 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:22-495:30 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:32-495:41 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:43-495:51 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:53-495:62 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:64-495:71 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:73-495:81 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:83-495:94 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:96-495:107 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:109-495:116 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:118-495:126 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:128-495:135 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:137-495:145 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:147-495:154 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:156-495:163 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:165-495:173 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:175-495:183 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:185-495:193 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 495:195-495:206 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 497:35-497:72 Type testdata/Builtins.lc 497:35-497:72 V3 testdata/Builtins.lc 497:39-497:48 'Nat -> Type->Type testdata/Builtins.lc 497:35-497:72 'Nat testdata/Builtins.lc 497:35-497:72 V1 testdata/Builtins.lc 497:51-497:56 Type testdata/Builtins.lc 497:1-497:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 497:10-497:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 500:35-500:67 Type testdata/Builtins.lc 500:35-500:67 V3 testdata/Builtins.lc 500:39-500:48 'Nat -> Type->Type testdata/Builtins.lc 500:35-500:67 'Nat testdata/Builtins.lc 500:35-500:67 V1 testdata/Builtins.lc 500:51-500:56 Type testdata/Builtins.lc 499:1-499:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 499:12-499:21 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 499:23-499:32 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 499:34-499:47 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 499:49-499:57 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 499:59-499:68 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 501:35-501:75 Type testdata/Builtins.lc 501:35-501:38 Type->Type testdata/Builtins.lc 501:35-501:75 V5 testdata/Builtins.lc 501:35-501:75 V4 testdata/Builtins.lc 501:46-501:55 'Nat -> Type->Type testdata/Builtins.lc 501:35-501:75 'Nat testdata/Builtins.lc 501:35-501:75 V2 testdata/Builtins.lc 501:1-501:8 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 501:10-501:17 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b testdata/Builtins.lc 502:35-502:75 Type testdata/Builtins.lc 502:35-502:38 Type->Type testdata/Builtins.lc 502:35-502:75 V5 testdata/Builtins.lc 502:35-502:75 V4 testdata/Builtins.lc 502:46-502:55 'Nat -> Type->Type testdata/Builtins.lc 502:35-502:75 'Nat testdata/Builtins.lc 502:35-502:75 V2 testdata/Builtins.lc 502:1-502:9 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 502:11-502:19 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b testdata/Builtins.lc 503:35-503:89 Type testdata/Builtins.lc 503:35-503:89 V5 testdata/Builtins.lc 503:39-503:48 'Nat -> Type->Type testdata/Builtins.lc 503:35-503:89 'Nat testdata/Builtins.lc 503:35-503:89 V3 testdata/Builtins.lc 503:51-503:56 Type testdata/Builtins.lc 503:35-503:89 V2 testdata/Builtins.lc 503:62-503:71 'Nat -> Type->Type testdata/Builtins.lc 503:74-503:78 Type testdata/Builtins.lc 503:1-503:10 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 503:12-503:21 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c testdata/Builtins.lc 504:35-504:73 Type testdata/Builtins.lc 504:35-504:41 Type->Type testdata/Builtins.lc 504:35-504:73 V5 testdata/Builtins.lc 504:35-504:73 V4 testdata/Builtins.lc 504:49-504:58 'Nat -> Type->Type testdata/Builtins.lc 504:35-504:73 'Nat testdata/Builtins.lc 504:35-504:73 V2 testdata/Builtins.lc 504:1-504:8 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 504:10-504:18 {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b testdata/Builtins.lc 505:35-505:72 Type testdata/Builtins.lc 505:35-505:72 V3 testdata/Builtins.lc 505:39-505:48 'Nat -> Type->Type testdata/Builtins.lc 505:35-505:72 'Nat testdata/Builtins.lc 505:35-505:72 V1 testdata/Builtins.lc 505:51-505:56 Type testdata/Builtins.lc 505:66-505:72 Type -> Type->Type testdata/Builtins.lc 505:1-505:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> 'Tuple2 a a testdata/Builtins.lc 506:35-506:80 Type testdata/Builtins.lc 506:35-506:38 Type->Type testdata/Builtins.lc 506:35-506:80 V5 testdata/Builtins.lc 506:35-506:80 V4 testdata/Builtins.lc 506:46-506:55 'Nat -> Type->Type testdata/Builtins.lc 506:35-506:80 'Nat testdata/Builtins.lc 506:35-506:80 V2 testdata/Builtins.lc 506:1-506:10 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b testdata/Builtins.lc 507:35-507:80 Type testdata/Builtins.lc 507:35-507:38 Type->Type testdata/Builtins.lc 507:35-507:80 V5 testdata/Builtins.lc 507:35-507:80 V4 testdata/Builtins.lc 507:46-507:55 'Nat -> Type->Type testdata/Builtins.lc 507:35-507:80 'Nat testdata/Builtins.lc 507:35-507:80 V2 testdata/Builtins.lc 507:1-507:11 {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b testdata/Builtins.lc 508:35-508:77 Type testdata/Builtins.lc 508:35-508:77 V3 testdata/Builtins.lc 508:39-508:48 'Nat -> Type->Type testdata/Builtins.lc 508:35-508:77 'Nat testdata/Builtins.lc 508:35-508:77 V1 testdata/Builtins.lc 508:51-508:56 Type testdata/Builtins.lc 508:1-508:8 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 509:35-509:81 Type testdata/Builtins.lc 509:35-509:81 V3 testdata/Builtins.lc 509:39-509:48 'Nat -> Type->Type testdata/Builtins.lc 509:35-509:81 'Nat testdata/Builtins.lc 509:35-509:81 V1 testdata/Builtins.lc 509:51-509:56 Type testdata/Builtins.lc 509:71-509:76 Type testdata/Builtins.lc 509:1-509:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a testdata/Builtins.lc 510:35-510:99 Type testdata/Builtins.lc 510:35-510:99 V5 testdata/Builtins.lc 510:39-510:48 'Nat -> Type->Type testdata/Builtins.lc 510:35-510:99 'Nat testdata/Builtins.lc 510:35-510:99 V3 testdata/Builtins.lc 510:51-510:56 Type testdata/Builtins.lc 510:35-510:99 V2 testdata/Builtins.lc 510:62-510:71 'Nat -> Type->Type testdata/Builtins.lc 510:74-510:78 Type testdata/Builtins.lc 510:1-510:9 {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a testdata/Builtins.lc 511:35-511:68 Type testdata/Builtins.lc 511:35-511:68 V3 testdata/Builtins.lc 511:39-511:44 'Nat -> Type->Type testdata/Builtins.lc 511:35-511:68 'Nat testdata/Builtins.lc 511:35-511:68 V1 testdata/Builtins.lc 511:47-511:52 Type testdata/Builtins.lc 511:1-511:9 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a testdata/Builtins.lc 512:35-512:76 Type testdata/Builtins.lc 512:35-512:76 V3 testdata/Builtins.lc 512:39-512:48 'Nat -> Type->Type testdata/Builtins.lc 512:35-512:76 'Nat testdata/Builtins.lc 512:35-512:76 V1 testdata/Builtins.lc 512:51-512:56 Type testdata/Builtins.lc 512:61-512:66 Type testdata/Builtins.lc 512:1-512:10 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a testdata/Builtins.lc 513:35-513:73 Type testdata/Builtins.lc 513:35-513:73 V3 testdata/Builtins.lc 513:39-513:44 'Nat -> Type->Type testdata/Builtins.lc 513:35-513:73 'Nat testdata/Builtins.lc 513:35-513:73 V1 testdata/Builtins.lc 513:47-513:52 Type testdata/Builtins.lc 513:1-513:15 {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a testdata/Builtins.lc 514:35-514:85 Type testdata/Builtins.lc 514:35-514:85 V3 testdata/Builtins.lc 514:39-514:48 'Nat -> Type->Type testdata/Builtins.lc 514:35-514:85 'Nat testdata/Builtins.lc 514:35-514:85 V1 testdata/Builtins.lc 514:51-514:56 Type testdata/Builtins.lc 514:61-514:66 Type testdata/Builtins.lc 514:70-514:75 Type testdata/Builtins.lc 514:1-514:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a testdata/Builtins.lc 517:34-517:70 Type testdata/Builtins.lc 517:34-517:43 'Nat -> Type->Type testdata/Builtins.lc 517:34-517:70 'Nat testdata/Builtins.lc 517:34-517:70 V1 testdata/Builtins.lc 517:46-517:51 Type testdata/Builtins.lc 517:55-517:64 'Nat -> Type->Type testdata/Builtins.lc 517:67-517:70 Type testdata/Builtins.lc 517:1-517:19 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int testdata/Builtins.lc 518:34-518:71 Type testdata/Builtins.lc 518:34-518:43 'Nat -> Type->Type testdata/Builtins.lc 518:34-518:71 'Nat testdata/Builtins.lc 518:34-518:71 V1 testdata/Builtins.lc 518:46-518:51 Type testdata/Builtins.lc 518:55-518:64 'Nat -> Type->Type testdata/Builtins.lc 518:67-518:71 Type testdata/Builtins.lc 518:1-518:20 {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word testdata/Builtins.lc 519:34-519:72 Type testdata/Builtins.lc 519:34-519:43 'Nat -> Type->Type testdata/Builtins.lc 519:34-519:72 'Nat testdata/Builtins.lc 519:34-519:72 V1 testdata/Builtins.lc 519:46-519:49 Type testdata/Builtins.lc 519:55-519:64 'Nat -> Type->Type testdata/Builtins.lc 519:67-519:72 Type testdata/Builtins.lc 519:1-519:19 {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float testdata/Builtins.lc 520:34-520:72 Type testdata/Builtins.lc 520:34-520:43 'Nat -> Type->Type testdata/Builtins.lc 520:34-520:72 'Nat testdata/Builtins.lc 520:34-520:72 V1 testdata/Builtins.lc 520:46-520:50 Type testdata/Builtins.lc 520:55-520:64 'Nat -> Type->Type testdata/Builtins.lc 520:67-520:72 Type testdata/Builtins.lc 520:1-520:20 {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float testdata/Builtins.lc 522:35-522:71 Type testdata/Builtins.lc 522:35-522:71 V3 testdata/Builtins.lc 522:39-522:48 'Nat -> Type->Type testdata/Builtins.lc 522:35-522:71 'Nat testdata/Builtins.lc 522:35-522:71 V1 testdata/Builtins.lc 522:51-522:56 Type testdata/Builtins.lc 522:66-522:71 Type testdata/Builtins.lc 522:1-522:11 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float testdata/Builtins.lc 523:35-523:76 Type testdata/Builtins.lc 523:35-523:76 V3 testdata/Builtins.lc 523:39-523:48 'Nat -> Type->Type testdata/Builtins.lc 523:35-523:76 'Nat testdata/Builtins.lc 523:35-523:76 V1 testdata/Builtins.lc 523:51-523:56 Type testdata/Builtins.lc 523:71-523:76 Type testdata/Builtins.lc 523:1-523:13 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 523:15-523:22 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float testdata/Builtins.lc 524:35-524:72 Type testdata/Builtins.lc 524:35-524:72 V1 testdata/Builtins.lc 524:39-524:56 Type testdata/Builtins.lc 524:39-524:48 'Nat -> Type->Type testdata/Builtins.lc 524:51-524:56 Type testdata/Builtins.lc 524:1-524:10 {a} -> {b : a ~ 'VecS 'Float (Succ (Succ (Succ Zero)))} -> a -> a->a testdata/Builtins.lc 525:35-525:67 Type testdata/Builtins.lc 525:35-525:67 V3 testdata/Builtins.lc 525:39-525:48 'Nat -> Type->Type testdata/Builtins.lc 525:35-525:67 'Nat testdata/Builtins.lc 525:35-525:67 V1 testdata/Builtins.lc 525:51-525:56 Type testdata/Builtins.lc 525:1-525:14 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 526:35-526:77 Type testdata/Builtins.lc 526:35-526:77 V3 testdata/Builtins.lc 526:39-526:48 'Nat -> Type->Type testdata/Builtins.lc 526:35-526:77 'Nat testdata/Builtins.lc 526:35-526:77 V1 testdata/Builtins.lc 526:51-526:56 Type testdata/Builtins.lc 526:1-526:16 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 526:18-526:29 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a testdata/Builtins.lc 527:35-527:72 Type testdata/Builtins.lc 527:35-527:72 V3 testdata/Builtins.lc 527:39-527:48 'Nat -> Type->Type testdata/Builtins.lc 527:35-527:72 'Nat testdata/Builtins.lc 527:35-527:72 V1 testdata/Builtins.lc 527:51-527:56 Type testdata/Builtins.lc 527:1-527:12 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a testdata/Builtins.lc 529:34-529:56 Type testdata/Builtins.lc 529:34-529:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 529:34-529:56 'Nat testdata/Builtins.lc 529:34-529:56 V5 testdata/Builtins.lc 529:34-529:56 V3 testdata/Builtins.lc 529:34-529:56 V1 testdata/Builtins.lc 529:47-529:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 529:1-529:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Mat b a c testdata/Builtins.lc 530:34-530:52 Type testdata/Builtins.lc 530:34-530:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 530:34-530:52 'Nat testdata/Builtins.lc 530:34-530:52 V3 testdata/Builtins.lc 530:34-530:52 V1 testdata/Builtins.lc 530:47-530:52 Type testdata/Builtins.lc 530:1-530:16 {a:'Nat} -> {b} -> 'Mat a a b -> 'Float testdata/Builtins.lc 531:34-531:56 Type testdata/Builtins.lc 531:34-531:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 531:34-531:56 'Nat testdata/Builtins.lc 531:34-531:56 V3 testdata/Builtins.lc 531:34-531:56 V1 testdata/Builtins.lc 531:47-531:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 531:1-531:12 {a:'Nat} -> {b} -> 'Mat a a b -> 'Mat a a b testdata/Builtins.lc 532:34-532:69 Type testdata/Builtins.lc 532:34-532:37 'Nat -> Type->Type testdata/Builtins.lc 532:34-532:69 'Nat testdata/Builtins.lc 532:34-532:69 V5 testdata/Builtins.lc 532:34-532:69 V3 testdata/Builtins.lc 532:47-532:50 'Nat -> Type->Type testdata/Builtins.lc 532:34-532:69 V2 testdata/Builtins.lc 532:60-532:63 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 532:1-532:17 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'VecS b c -> 'Mat c a b testdata/Builtins.lc 533:34-533:67 Type testdata/Builtins.lc 533:34-533:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 533:34-533:67 'Nat testdata/Builtins.lc 533:34-533:67 V5 testdata/Builtins.lc 533:34-533:67 V3 testdata/Builtins.lc 533:34-533:67 V1 testdata/Builtins.lc 533:47-533:50 'Nat -> Type->Type testdata/Builtins.lc 533:60-533:63 'Nat -> Type->Type testdata/Builtins.lc 533:1-533:14 {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'VecS c b -> 'VecS c a testdata/Builtins.lc 534:34-534:67 Type testdata/Builtins.lc 534:34-534:37 'Nat -> Type->Type testdata/Builtins.lc 534:34-534:67 'Nat testdata/Builtins.lc 534:34-534:67 V5 testdata/Builtins.lc 534:34-534:67 V3 testdata/Builtins.lc 534:47-534:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 534:34-534:67 V2 testdata/Builtins.lc 534:60-534:63 'Nat -> Type->Type testdata/Builtins.lc 534:1-534:14 {a:'Nat} -> {b} -> {c:'Nat} -> 'VecS b a -> 'Mat a c b -> 'VecS b c testdata/Builtins.lc 535:34-535:69 Type testdata/Builtins.lc 535:34-535:37 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 535:34-535:69 'Nat testdata/Builtins.lc 535:34-535:69 V7 testdata/Builtins.lc 535:34-535:69 V5 testdata/Builtins.lc 535:34-535:69 V3 testdata/Builtins.lc 535:47-535:50 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 535:34-535:69 V2 testdata/Builtins.lc 535:60-535:63 'Nat -> 'Nat -> Type->Type testdata/Builtins.lc 535:1-535:14 {a:'Nat} -> {b:'Nat} -> {c} -> {d:'Nat} -> 'Mat a b c -> 'Mat b d c -> 'Mat a d c testdata/Builtins.lc 538:35-538:97 Type testdata/Builtins.lc 538:35-538:38 Type->Type testdata/Builtins.lc 538:35-538:97 V7 testdata/Builtins.lc 538:35-538:97 V6 testdata/Builtins.lc 538:46-538:55 'Nat -> Type->Type testdata/Builtins.lc 538:35-538:97 'Nat testdata/Builtins.lc 538:35-538:97 V4 testdata/Builtins.lc 538:35-538:97 V3 testdata/Builtins.lc 538:65-538:74 'Nat -> Type->Type testdata/Builtins.lc 538:77-538:81 Type testdata/Builtins.lc 537:1-537:13 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 537:15-537:32 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 537:34-537:49 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 537:51-537:71 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 537:73-537:83 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 537:85-537:98 {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Num a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Bool} -> b -> b->d testdata/Builtins.lc 539:35-539:76 Type testdata/Builtins.lc 539:35-539:76 V3 testdata/Builtins.lc 539:39-539:55 Type->Type testdata/Builtins.lc 539:35-539:76 V1 testdata/Builtins.lc 539:72-539:76 Type testdata/Builtins.lc 539:1-539:10 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 539:12-539:24 {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> b -> b->'Bool testdata/Builtins.lc 542:35-542:67 Type testdata/Builtins.lc 542:35-542:67 V3 testdata/Builtins.lc 542:39-542:48 'Nat -> Type->Type testdata/Builtins.lc 542:35-542:67 'Nat testdata/Builtins.lc 542:35-542:67 V1 testdata/Builtins.lc 542:51-542:56 Type testdata/Builtins.lc 541:1-541:9 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 541:11-541:19 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 541:21-541:31 {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a testdata/Builtins.lc 544:34-544:60 Type testdata/Builtins.lc 544:34-544:43 'Nat -> Type->Type testdata/Builtins.lc 544:34-544:60 'Nat testdata/Builtins.lc 544:34-544:60 V1 testdata/Builtins.lc 544:46-544:51 Type testdata/Builtins.lc 544:55-544:60 Type testdata/Builtins.lc 544:1-544:11 {a:'Nat} -> 'VecScalar a 'Float -> 'Float testdata/Builtins.lc 545:34-545:66 Type testdata/Builtins.lc 545:34-545:43 'Nat -> Type->Type testdata/Builtins.lc 545:34-545:66 'Nat testdata/Builtins.lc 545:34-545:66 V1 testdata/Builtins.lc 545:46-545:51 Type testdata/Builtins.lc 545:55-545:66 Type testdata/Builtins.lc 545:55-545:58 'Nat -> Type->Type testdata/Builtins.lc 545:61-545:66 Type testdata/Builtins.lc 545:1-545:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ Zero)) testdata/Builtins.lc 546:34-546:66 Type testdata/Builtins.lc 546:34-546:43 'Nat -> Type->Type testdata/Builtins.lc 546:34-546:66 'Nat testdata/Builtins.lc 546:34-546:66 V1 testdata/Builtins.lc 546:46-546:51 Type testdata/Builtins.lc 546:55-546:66 Type testdata/Builtins.lc 546:55-546:58 'Nat -> Type->Type testdata/Builtins.lc 546:61-546:66 Type testdata/Builtins.lc 546:1-546:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ Zero))) testdata/Builtins.lc 547:34-547:66 Type testdata/Builtins.lc 547:34-547:43 'Nat -> Type->Type testdata/Builtins.lc 547:34-547:66 'Nat testdata/Builtins.lc 547:34-547:66 V1 testdata/Builtins.lc 547:46-547:51 Type testdata/Builtins.lc 547:55-547:66 Type testdata/Builtins.lc 547:55-547:58 'Nat -> Type->Type testdata/Builtins.lc 547:61-547:66 Type testdata/Builtins.lc 547:1-547:11 {a:'Nat} -> 'VecScalar a 'Float -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 563:6-563:13 Type testdata/Builtins.lc 564:20-564:26 Type testdata/Builtins.lc 565:20-565:27 Type testdata/Builtins.lc 564:3-564:16 'String->'Texture testdata/Builtins.lc 567:20-567:23 'Nat -> Type->Type testdata/Builtins.lc 567:26-567:29 Type testdata/Builtins.lc 568:20-569:27 Type testdata/Builtins.lc 568:20-568:25 'Nat -> Type->Type testdata/Builtins.lc 568:29-568:47 Type testdata/Builtins.lc 568:29-568:34 Type->Type testdata/Builtins.lc 568:36-568:47 Type testdata/Builtins.lc 568:36-568:39 'Nat -> Type->Type testdata/Builtins.lc 568:42-568:47 Type testdata/Builtins.lc 569:20-569:27 Type testdata/Builtins.lc 567:3-567:12 'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture testdata/Builtins.lc 571:6-571:12 Type testdata/Builtins.lc 572:5-572:16 'Filter testdata/Builtins.lc 573:5-573:17 'Filter testdata/Builtins.lc 575:6-575:14 Type testdata/Builtins.lc 576:5-576:11 'EdgeMode testdata/Builtins.lc 577:5-577:19 'EdgeMode testdata/Builtins.lc 578:5-578:16 'EdgeMode testdata/Builtins.lc 580:6-580:13 Type testdata/Builtins.lc 580:24-580:30 Type testdata/Builtins.lc 580:6-580:47 Type testdata/Builtins.lc 580:31-580:39 Type testdata/Builtins.lc 580:40-580:47 Type testdata/Builtins.lc 580:16-580:23 'Filter -> 'EdgeMode -> 'Texture->'Sampler testdata/Builtins.lc 583:14-583:21 Type testdata/Builtins.lc 583:25-583:51 Type testdata/Builtins.lc 583:25-583:28 'Nat -> Type->Type testdata/Builtins.lc 583:31-583:36 Type testdata/Builtins.lc 583:40-583:51 Type testdata/Builtins.lc 583:40-583:43 'Nat -> Type->Type testdata/Builtins.lc 583:46-583:51 Type testdata/Builtins.lc 583:1-583:10 'Sampler -> 'VecS 'Float (Succ (Succ Zero)) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) testdata/Builtins.lc 586:30-586:45 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b testdata/Builtins.lc 586:47-586:66 V1 -> 'Stream V1 testdata/Builtins.lc 586:47-586:57 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) testdata/Builtins.lc 586:59-586:66 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType V1) -> 'Float testdata/Builtins.lc 586:65-586:66 'Float testdata/Builtins.lc 586:65-586:66 'Int testdata/Builtins.lc 586:1-586:20 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) testdata/Builtins.lc 587:46-587:61 {a} -> {b} -> (a -> 'Stream b) -> 'Stream a -> 'Stream b testdata/Builtins.lc 587:63-587:73 V1 -> 'Stream V1 testdata/Builtins.lc 587:63-587:73 {a} -> {b} -> {c} -> {d:'PrimitiveType} -> {e : a ~ 'InterpolatedType b} -> {f : c ~ 'JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) a} -> c->'Float -> b -> 'RasterContext d -> 'Primitive d c -> 'Stream ('Fragment (Succ Zero) DefinedDepth a) testdata/Builtins.lc 587:1-587:33 {a} -> {b:'PrimitiveType} -> 'RasterContext b -> ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a) -> 'Float) -> a -> 'Stream ('Primitive b ('JoinTupleType ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))) ('InterpolatedType a))) -> 'Stream ('Fragment (Succ Zero) DefinedDepth ('InterpolatedType a)) testdata/Builtins.lc 588:24-588:32 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 588:1-588:15 {a} -> {b} -> a -> b -> 'Tuple2 a b testdata/Builtins.lc 589:25-589:35 V2 -> V2->V2 testdata/Builtins.lc 589:25-589:35 V2->V2 testdata/Builtins.lc 589:25-589:35 V2 testdata/Builtins.lc 589:25-589:35 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FragOps' b -> 'Stream ('Fragment a c ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b testdata/Builtins.lc 589:13-589:21 'Tuple2 ('FragOps' V1) ('Stream ('Fragment V2 V0 ('RemSemantics V1))) testdata/Builtins.lc 589:13-589:21 V4 testdata/Builtins.lc 589:1-589:8 {a:'Nat} -> {b} -> {c:'DepthHandler} -> 'FrameBuffer a b -> 'Tuple2 ('FragOps' b) ('Stream ('Fragment a c ('RemSemantics b))) -> 'FrameBuffer a b testdata/Builtins.lc 590:15-590:24 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 590:1-590:12 {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output testdata/Builtins.lc 591:14-591:25 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 591:1-591:11 {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b testdata/Builtins.lc 592:19-592:29 {a:'Nat} -> 'Float -> 'Image a ('Depth 'Float) testdata/Builtins.lc 592:1-592:16 'Float -> 'Image (Succ Zero) ('Depth 'Float) testdata/Builtins.lc 593:19-593:29 {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a ('Color d) testdata/Builtins.lc 593:1-593:16 {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image (Succ Zero) ('Color c)