summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPéter Diviánszky <divipp@gmail.com>2016-02-05 16:35:12 +0100
committerPéter Diviánszky <divipp@gmail.com>2016-02-05 17:55:41 +0100
commite19b4e7051066ce8bff0e4b3c51b06e1169d4fb1 (patch)
tree0c4a2078c30f2faf7ee83ed4a78d4028cc34e6c1
parentae0343e3053c5d8b9301f4f43b35a7a4f9c05dcf (diff)
refactor Builtins.lc
Diffstat
-rw-r--r--lc/Builtins.lc27
-rw-r--r--src/LambdaCube/Compiler/CoreToIR.hs6
-rw-r--r--src/LambdaCube/Compiler/Infer.hs4
-rw-r--r--testdata/Builtins.out2116
4 files changed, 1073 insertions, 1080 deletions
diff --git a/lc/Builtins.lc b/lc/Builtins.lc
index a8b9e98b..80a818eb 100644
--- a/lc/Builtins.lc
+++ b/lc/Builtins.lc
@@ -295,12 +295,12 @@ type family FragOps a where
295 FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) = (t1, t2, t3, t4) 295 FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) = (t1, t2, t3, t4)
296 FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) = (t1, t2, t3, t4, t5) 296 FragOps (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) = (t1, t2, t3, t4, t5)
297-} 297-}
298type family FragOps' a where 298type family FragOps a where
299 FragOps' (t1, t2) = (FragmentOperation t1, FragmentOperation t2) 299 FragOps (t1, t2) = (FragmentOperation t1, FragmentOperation t2)
300 FragOps' (t1, t2, t3) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3) 300 FragOps (t1, t2, t3) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3)
301 FragOps' (t1, t2, t3, t4) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4) 301 FragOps (t1, t2, t3, t4) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4)
302 FragOps' (t1, t2, t3, t4, t5) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5) 302 FragOps (t1, t2, t3, t4, t5) = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5)
303 FragOps' t = (FragmentOperation t) 303 FragOps t = (FragmentOperation t)
304 304
305[] ++ ys = ys 305[] ++ ys = ys
306x:xs ++ ys = x : xs ++ ys 306x:xs ++ ys = x : xs ++ ys
@@ -407,11 +407,12 @@ rasterize
407 407
408rasterizePrimitives ctx is s = concat (map (rasterize is ctx) s) 408rasterizePrimitives ctx is s = concat (map (rasterize is ctx) s)
409 409
410data Image :: Nat -> Type -> Type where 410data Image :: Nat -> Type -> Type
411 ColorImage :: forall a d t color . (Num t, color ~ VecScalar d t) 411
412 => color -> Image a (Color color) 412ColorImage :: forall a d t color . (Num t, color ~ VecScalar d t)
413 DepthImage :: forall a . Float -> Image a (Depth Float) 413 => color -> Image a (Color color)
414 StencilImage :: forall a . Int -> Image a (Stencil Int) 414DepthImage :: forall a . Float -> Image a (Depth Float)
415StencilImage :: forall a . Int -> Image a (Stencil Int)
415 416
416type family SameLayerCounts a where 417type family SameLayerCounts a where
417 SameLayerCounts (Image n1 t1) = Unit 418 SameLayerCounts (Image n1 t1) = Unit
@@ -427,8 +428,8 @@ instance (DefaultFragOp a, DefaultFragOp b) => DefaultFragOps (FragmentOperation
427 defaultFragOps = -- (undefined @(), undefined) 428 defaultFragOps = -- (undefined @(), undefined)
428 (defaultFragOp @a @_, defaultFragOp @b @_) 429 (defaultFragOp @a @_, defaultFragOp @b @_)
429-} 430-}
430data FrameBuffer (n :: Nat) b where 431data FrameBuffer (n :: Nat) t
431 Accumulate :: FragOps' b -> FragmentStream n (RemSemantics b) -> FrameBuffer n b -> FrameBuffer n b 432Accumulate :: FragOps b -> FragmentStream n (RemSemantics b) -> FrameBuffer n b -> FrameBuffer n b
432 433
433type family TFFrameBuffer a where 434type family TFFrameBuffer a where
434 TFFrameBuffer (Image n1 t1) = FrameBuffer n1 t1 435 TFFrameBuffer (Image n1 t1) = FrameBuffer n1 t1
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 9c67cb02..2a3c78eb 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -225,7 +225,7 @@ getCommands e = case e of
225 rt <- newFrameBufferTarget (tyOf a) 225 rt <- newFrameBufferTarget (tyOf a)
226 (subCmds,cmds) <- getCommands a 226 (subCmds,cmds) <- getCommands a
227 return (subCmds,IR.SetRenderTarget rt : cmds) 227 return (subCmds,IR.SetRenderTarget rt : cmds)
228 A3 "Accumulate" actx (getFragmentShader . removeDepthHandler -> (frag, getFragFilter -> (ffilter, Prim3 "foldr" (EtaPrim2_2 "++") (A0 "Nil") (Prim2 "map" (EtaPrim3 "rasterize" {-rp-} is rctx) (getVertexShader -> (vert, input)))))) fbuf -> do 228 Prim3 "Accumulate" actx (getFragmentShader . removeDepthHandler -> (frag, getFragFilter -> (ffilter, Prim3 "foldr" (EtaPrim2_2 "++") (A0 "Nil") (Prim2 "map" (EtaPrim3 "rasterize" {-rp-} is rctx) (getVertexShader -> (vert, input)))))) fbuf -> do
229 let rp = compRC' rctx 229 let rp = compRC' rctx
230 (smpBindingsV,vertCmds) <- getRenderTextureCommands vert 230 (smpBindingsV,vertCmds) <- getRenderTextureCommands vert
231 (smpBindingsR,rastCmds) <- maybe (return mempty) getRenderTextureCommands ffilter 231 (smpBindingsR,rastCmds) <- maybe (return mempty) getRenderTextureCommands ffilter
@@ -267,8 +267,8 @@ getUniforms e = case e of
267 267
268compFrameBuffer x = case x of 268compFrameBuffer x = case x of
269 ETuple a -> concatMap compFrameBuffer a 269 ETuple a -> concatMap compFrameBuffer a
270 A1 "DepthImage" a -> [(IR.Depth, compValue a)] 270 Prim1 "DepthImage" a -> [(IR.Depth, compValue a)]
271 A1 "ColorImage" a -> [(IR.Color, compValue a)] 271 Prim1 "ColorImage" a -> [(IR.Color, compValue a)]
272 x -> error $ "compFrameBuffer " ++ ppShow x 272 x -> error $ "compFrameBuffer " ++ ppShow x
273 273
274compSemantic x = case x of 274compSemantic x = case x of
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 3df27eaa..70fab42f 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -574,8 +574,8 @@ cstrT_ typ = cstr__ []
574 cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) 574 cstr_ [] (UL (FunN "'VecScalar" [a, b])) t@(TTyCon0 n) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t)
575 cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t) 575 cstr_ [] t@(TTyCon0 n) (UL (FunN "'VecScalar" [a, b])) | isElemTy n = t2 (cstrT TNat a (ENat 1)) (cstr__ [] b t)
576 576
577 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x 577 cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'FragmentOperation" [x]) = cstr__ ns a x
578 cstr_ ns@[] (UL (FunN "'FragOps'" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y 578 cstr_ ns@[] (UL (FunN "'FragOps" [a])) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = cstr__ ns a $ TTuple2 x y
579 579
580 cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y') 580 cstr_ ns@[] (TyConN "'Tuple2" [x, y]) (UL (FunN "'JoinTupleType" [x', y'])) = t2 (cstr__ ns x x') (cstr__ ns y y')
581 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y) 581 cstr_ ns@[] (UL (FunN "'JoinTupleType" [x', y'])) (TyConN "'Tuple2" [x, y]) = t2 (cstr__ ns x' x) (cstr__ ns y' y)
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index e982ec21..d93f0422 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -972,74 +972,74 @@ testdata/Builtins.lc 289:71-289:104 Type
972testdata/Builtins.lc 289:89-289:104 Type 972testdata/Builtins.lc 289:89-289:104 Type
973testdata/Builtins.lc 289:90-289:97 Type->Type 973testdata/Builtins.lc 289:90-289:97 Type->Type
974testdata/Builtins.lc 289:98-289:103 Type 974testdata/Builtins.lc 289:98-289:103 Type
975testdata/Builtins.lc 299:5-299:13 Type->Type 975testdata/Builtins.lc 299:5-299:12 Type->Type
976testdata/Builtins.lc 299:15-299:21 Type 976testdata/Builtins.lc 299:14-299:20 Type
977testdata/Builtins.lc 299:15-299:69 Type->Type 977testdata/Builtins.lc 299:14-299:68 Type->Type
978testdata/Builtins.lc 299:15-303:39 Type | Type->Type 978testdata/Builtins.lc 299:14-303:38 Type | Type->Type
979testdata/Builtins.lc 299:25-299:69 Type | Type -> Type->Type | Type->Type 979testdata/Builtins.lc 299:24-299:68 Type | Type -> Type->Type | Type->Type
980testdata/Builtins.lc 299:26-299:43 Type->Type 980testdata/Builtins.lc 299:25-299:42 Type->Type
981testdata/Builtins.lc 299:26-299:46 Type 981testdata/Builtins.lc 299:25-299:45 Type
982testdata/Builtins.lc 299:44-299:46 Type 982testdata/Builtins.lc 299:43-299:45 Type
983testdata/Builtins.lc 299:48-299:65 Type->Type 983testdata/Builtins.lc 299:47-299:64 Type->Type
984testdata/Builtins.lc 299:48-299:68 Type 984testdata/Builtins.lc 299:47-299:67 Type
985testdata/Builtins.lc 299:66-299:68 Type 985testdata/Builtins.lc 299:65-299:67 Type
986testdata/Builtins.lc 300:15-300:25 Type 986testdata/Builtins.lc 300:14-300:24 Type
987testdata/Builtins.lc 300:15-300:95 Type->Type 987testdata/Builtins.lc 300:14-300:94 Type->Type
988testdata/Builtins.lc 300:15-303:39 Type 988testdata/Builtins.lc 300:14-303:38 Type
989testdata/Builtins.lc 300:29-300:95 Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type 989testdata/Builtins.lc 300:28-300:94 Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type
990testdata/Builtins.lc 300:30-300:47 Type->Type 990testdata/Builtins.lc 300:29-300:46 Type->Type
991testdata/Builtins.lc 300:30-300:50 Type 991testdata/Builtins.lc 300:29-300:49 Type
992testdata/Builtins.lc 300:30-300:72 Type->Type 992testdata/Builtins.lc 300:29-300:71 Type->Type
993testdata/Builtins.lc 300:48-300:50 Type 993testdata/Builtins.lc 300:47-300:49 Type
994testdata/Builtins.lc 300:52-300:69 Type->Type 994testdata/Builtins.lc 300:51-300:68 Type->Type
995testdata/Builtins.lc 300:52-300:72 Type 995testdata/Builtins.lc 300:51-300:71 Type
996testdata/Builtins.lc 300:70-300:72 Type 996testdata/Builtins.lc 300:69-300:71 Type
997testdata/Builtins.lc 300:74-300:91 Type->Type 997testdata/Builtins.lc 300:73-300:90 Type->Type
998testdata/Builtins.lc 300:74-300:94 Type 998testdata/Builtins.lc 300:73-300:93 Type
999testdata/Builtins.lc 300:92-300:94 Type 999testdata/Builtins.lc 300:91-300:93 Type
1000testdata/Builtins.lc 301:15-301:29 Type 1000testdata/Builtins.lc 301:14-301:28 Type
1001testdata/Builtins.lc 301:15-301:122 Type->Type 1001testdata/Builtins.lc 301:14-301:121 Type->Type
1002testdata/Builtins.lc 301:15-303:39 Type 1002testdata/Builtins.lc 301:14-303:38 Type
1003testdata/Builtins.lc 301:34-301:122 Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type 1003testdata/Builtins.lc 301:33-301:121 Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type
1004testdata/Builtins.lc 301:35-301:52 Type->Type 1004testdata/Builtins.lc 301:34-301:51 Type->Type
1005testdata/Builtins.lc 301:35-301:55 Type 1005testdata/Builtins.lc 301:34-301:54 Type
1006testdata/Builtins.lc 301:35-301:77 Type -> Type->Type 1006testdata/Builtins.lc 301:34-301:76 Type -> Type->Type
1007testdata/Builtins.lc 301:35-301:99 Type->Type 1007testdata/Builtins.lc 301:34-301:98 Type->Type
1008testdata/Builtins.lc 301:53-301:55 Type 1008testdata/Builtins.lc 301:52-301:54 Type
1009testdata/Builtins.lc 301:57-301:74 Type->Type 1009testdata/Builtins.lc 301:56-301:73 Type->Type
1010testdata/Builtins.lc 301:57-301:77 Type 1010testdata/Builtins.lc 301:56-301:76 Type
1011testdata/Builtins.lc 301:75-301:77 Type 1011testdata/Builtins.lc 301:74-301:76 Type
1012testdata/Builtins.lc 301:79-301:96 Type->Type 1012testdata/Builtins.lc 301:78-301:95 Type->Type
1013testdata/Builtins.lc 301:79-301:99 Type 1013testdata/Builtins.lc 301:78-301:98 Type
1014testdata/Builtins.lc 301:97-301:99 Type 1014testdata/Builtins.lc 301:96-301:98 Type
1015testdata/Builtins.lc 301:101-301:118 Type->Type 1015testdata/Builtins.lc 301:100-301:117 Type->Type
1016testdata/Builtins.lc 301:101-301:121 Type 1016testdata/Builtins.lc 301:100-301:120 Type
1017testdata/Builtins.lc 301:119-301:121 Type 1017testdata/Builtins.lc 301:118-301:120 Type
1018testdata/Builtins.lc 302:15-302:33 Type 1018testdata/Builtins.lc 302:14-302:32 Type
1019testdata/Builtins.lc 302:15-302:148 Type->Type 1019testdata/Builtins.lc 302:14-302:147 Type->Type
1020testdata/Builtins.lc 302:15-303:39 Type 1020testdata/Builtins.lc 302:14-303:38 Type
1021testdata/Builtins.lc 302:38-302:148 Type | Type -> Type -> Type -> Type -> Type->Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type 1021testdata/Builtins.lc 302:37-302:147 Type | Type -> Type -> Type -> Type -> Type->Type | Type -> Type -> Type -> Type->Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type
1022testdata/Builtins.lc 302:39-302:56 Type->Type 1022testdata/Builtins.lc 302:38-302:55 Type->Type
1023testdata/Builtins.lc 302:39-302:59 Type 1023testdata/Builtins.lc 302:38-302:58 Type
1024testdata/Builtins.lc 302:39-302:81 Type -> Type -> Type->Type 1024testdata/Builtins.lc 302:38-302:80 Type -> Type -> Type->Type
1025testdata/Builtins.lc 302:39-302:103 Type -> Type->Type 1025testdata/Builtins.lc 302:38-302:102 Type -> Type->Type
1026testdata/Builtins.lc 302:39-302:125 Type->Type 1026testdata/Builtins.lc 302:38-302:124 Type->Type
1027testdata/Builtins.lc 302:57-302:59 Type 1027testdata/Builtins.lc 302:56-302:58 Type
1028testdata/Builtins.lc 302:61-302:78 Type->Type 1028testdata/Builtins.lc 302:60-302:77 Type->Type
1029testdata/Builtins.lc 302:61-302:81 Type 1029testdata/Builtins.lc 302:60-302:80 Type
1030testdata/Builtins.lc 302:79-302:81 Type 1030testdata/Builtins.lc 302:78-302:80 Type
1031testdata/Builtins.lc 302:83-302:100 Type->Type 1031testdata/Builtins.lc 302:82-302:99 Type->Type
1032testdata/Builtins.lc 302:83-302:103 Type 1032testdata/Builtins.lc 302:82-302:102 Type
1033testdata/Builtins.lc 302:101-302:103 Type 1033testdata/Builtins.lc 302:100-302:102 Type
1034testdata/Builtins.lc 302:105-302:122 Type->Type 1034testdata/Builtins.lc 302:104-302:121 Type->Type
1035testdata/Builtins.lc 302:105-302:125 Type 1035testdata/Builtins.lc 302:104-302:124 Type
1036testdata/Builtins.lc 302:123-302:125 Type 1036testdata/Builtins.lc 302:122-302:124 Type
1037testdata/Builtins.lc 302:127-302:144 Type->Type 1037testdata/Builtins.lc 302:126-302:143 Type->Type
1038testdata/Builtins.lc 302:127-302:147 Type 1038testdata/Builtins.lc 302:126-302:146 Type
1039testdata/Builtins.lc 302:145-302:147 Type 1039testdata/Builtins.lc 302:144-302:146 Type
1040testdata/Builtins.lc 303:18-303:39 Type 1040testdata/Builtins.lc 303:17-303:38 Type
1041testdata/Builtins.lc 303:19-303:36 Type->Type 1041testdata/Builtins.lc 303:18-303:35 Type->Type
1042testdata/Builtins.lc 303:37-303:38 Type 1042testdata/Builtins.lc 303:36-303:37 Type
1043testdata/Builtins.lc 305:6-305:8 {a} -> List a -> List a -> List a 1043testdata/Builtins.lc 305:6-305:8 {a} -> List a -> List a -> List a
1044testdata/Builtins.lc 305:14-305:16 V3 1044testdata/Builtins.lc 305:14-305:16 V3
1045testdata/Builtins.lc 305:14-306:26 List V0 -> List V1 | V0->V1 1045testdata/Builtins.lc 305:14-306:26 List V0 -> List V1 | V0->V1
@@ -1516,330 +1516,301 @@ testdata/Builtins.lc 408:55-408:57 V8
1516testdata/Builtins.lc 408:58-408:61 V7 1516testdata/Builtins.lc 408:58-408:61 V7
1517testdata/Builtins.lc 408:63-408:64 V2 1517testdata/Builtins.lc 408:63-408:64 V2
1518testdata/Builtins.lc 410:6-410:11 Nat -> Type->Type | Type 1518testdata/Builtins.lc 410:6-410:11 Nat -> Type->Type | Type
1519testdata/Builtins.lc 410:6-414:68 Type
1520testdata/Builtins.lc 410:15-410:18 Type 1519testdata/Builtins.lc 410:15-410:18 Type
1521testdata/Builtins.lc 410:22-410:26 Type 1520testdata/Builtins.lc 410:22-410:26 Type
1522testdata/Builtins.lc 410:22-410:34 Type 1521testdata/Builtins.lc 410:22-410:34 Type
1523testdata/Builtins.lc 410:30-410:34 Type 1522testdata/Builtins.lc 410:30-410:34 Type
1524testdata/Builtins.lc 411:3-411:13 Image V6 (Color V3) | {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) 1523testdata/Builtins.lc 412:1-412:11 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d)
1525testdata/Builtins.lc 411:3-412:57 Type 1524testdata/Builtins.lc 412:45-413:55 Type
1526testdata/Builtins.lc 411:47-412:57 Type 1525testdata/Builtins.lc 412:46-412:49 Type->Type
1527testdata/Builtins.lc 411:48-411:51 Type->Type 1526testdata/Builtins.lc 412:46-412:51 Type
1528testdata/Builtins.lc 411:48-411:53 Type 1527testdata/Builtins.lc 412:50-412:51 V3
1529testdata/Builtins.lc 411:52-411:53 V3 1528testdata/Builtins.lc 412:53-412:58 V2
1530testdata/Builtins.lc 411:55-411:60 V2 1529testdata/Builtins.lc 412:53-412:60 Type->Type
1531testdata/Builtins.lc 411:55-411:62 Type->Type 1530testdata/Builtins.lc 412:53-412:74 Type
1532testdata/Builtins.lc 411:55-411:76 Type 1531testdata/Builtins.lc 412:53-413:55 Type
1533testdata/Builtins.lc 411:55-412:57 Type 1532testdata/Builtins.lc 412:59-412:60 Type -> Type->Type
1534testdata/Builtins.lc 411:61-411:62 Type -> Type->Type 1533testdata/Builtins.lc 412:61-412:70 Nat -> Type->Type
1535testdata/Builtins.lc 411:63-411:72 Nat -> Type->Type 1534testdata/Builtins.lc 412:61-412:72 Type->Type
1536testdata/Builtins.lc 411:63-411:74 Type->Type 1535testdata/Builtins.lc 412:61-412:74 Type
1537testdata/Builtins.lc 411:63-411:76 Type 1536testdata/Builtins.lc 412:71-412:72 V4
1538testdata/Builtins.lc 411:73-411:74 V4 1537testdata/Builtins.lc 412:73-412:74 Type
1539testdata/Builtins.lc 411:75-411:76 Type 1538testdata/Builtins.lc 413:24-413:29 Type
1540testdata/Builtins.lc 412:26-412:31 Type 1539testdata/Builtins.lc 413:24-413:55 Type
1541testdata/Builtins.lc 412:26-412:57 Type 1540testdata/Builtins.lc 413:34-413:39 Nat -> Type->Type
1542testdata/Builtins.lc 412:36-412:41 Nat -> Type->Type 1541testdata/Builtins.lc 413:34-413:41 Type->Type
1543testdata/Builtins.lc 412:36-412:43 Type->Type 1542testdata/Builtins.lc 413:34-413:55 Type
1544testdata/Builtins.lc 412:36-412:57 Type 1543testdata/Builtins.lc 413:40-413:41 V7
1545testdata/Builtins.lc 412:42-412:43 Nat | V7 1544testdata/Builtins.lc 413:42-413:55 Type
1546testdata/Builtins.lc 412:42-412:57 Image V6 (Color V3) -> Type 1545testdata/Builtins.lc 413:43-413:48 Type->Type
1547testdata/Builtins.lc 412:44-412:57 Type 1546testdata/Builtins.lc 413:49-413:54 Type
1548testdata/Builtins.lc 412:45-412:50 Type->Type 1547testdata/Builtins.lc 414:1-414:11 {a:Nat} -> Float -> Image a (Depth Float)
1549testdata/Builtins.lc 412:51-412:56 Type 1548testdata/Builtins.lc 414:35-414:40 Type
1550testdata/Builtins.lc 413:3-413:13 Image V1 (Depth Float) | {a:Nat} -> Float -> Image a (Depth Float) 1549testdata/Builtins.lc 414:35-414:66 Type
1551testdata/Builtins.lc 413:3-413:68 Type 1550testdata/Builtins.lc 414:45-414:50 Nat -> Type->Type
1552testdata/Builtins.lc 413:37-413:42 Type 1551testdata/Builtins.lc 414:45-414:52 Type->Type
1553testdata/Builtins.lc 413:37-413:68 Type 1552testdata/Builtins.lc 414:45-414:66 Type
1554testdata/Builtins.lc 413:47-413:52 Nat -> Type->Type 1553testdata/Builtins.lc 414:51-414:52 V2
1555testdata/Builtins.lc 413:47-413:54 Type->Type 1554testdata/Builtins.lc 414:53-414:66 Type
1556testdata/Builtins.lc 413:47-413:68 Type 1555testdata/Builtins.lc 414:54-414:59 Type->Type
1557testdata/Builtins.lc 413:53-413:54 Nat | V2 1556testdata/Builtins.lc 414:60-414:65 Type
1558testdata/Builtins.lc 413:53-413:68 Image V1 (Depth Float) -> Type 1557testdata/Builtins.lc 415:1-415:13 {a:Nat} -> Int -> Image a (Stencil Int)
1559testdata/Builtins.lc 413:55-413:68 Type 1558testdata/Builtins.lc 415:35-415:38 Type
1560testdata/Builtins.lc 413:56-413:61 Type->Type 1559testdata/Builtins.lc 415:35-415:66 Type
1561testdata/Builtins.lc 413:62-413:67 Type 1560testdata/Builtins.lc 415:45-415:50 Nat -> Type->Type
1562testdata/Builtins.lc 414:3-414:15 Image V1 (Stencil Int) | {a:Nat} -> Int -> Image a (Stencil Int) 1561testdata/Builtins.lc 415:45-415:52 Type->Type
1563testdata/Builtins.lc 414:3-414:68 Type 1562testdata/Builtins.lc 415:45-415:66 Type
1564testdata/Builtins.lc 414:37-414:40 Type 1563testdata/Builtins.lc 415:51-415:52 V2
1565testdata/Builtins.lc 414:37-414:68 Type 1564testdata/Builtins.lc 415:53-415:66 Type
1566testdata/Builtins.lc 414:47-414:52 Nat -> Type->Type 1565testdata/Builtins.lc 415:54-415:61 Type->Type
1567testdata/Builtins.lc 414:47-414:54 Type->Type 1566testdata/Builtins.lc 415:62-415:65 Type
1568testdata/Builtins.lc 414:47-414:68 Type 1567testdata/Builtins.lc 418:5-418:20 Type->Type
1569testdata/Builtins.lc 414:53-414:54 Nat | V2 1568testdata/Builtins.lc 418:28-418:33 Type
1570testdata/Builtins.lc 414:53-414:68 Image V1 (Stencil Int) -> Type 1569testdata/Builtins.lc 418:28-418:41 Type->Type
1571testdata/Builtins.lc 414:55-414:68 Type 1570testdata/Builtins.lc 418:28-420:99 Type | Type->Type
1572testdata/Builtins.lc 414:56-414:63 Type->Type 1571testdata/Builtins.lc 418:37-418:41 Nat -> Type->Type | Type | Type->Type
1573testdata/Builtins.lc 414:64-414:67 Type 1572testdata/Builtins.lc 419:22-419:46 Type
1574testdata/Builtins.lc 417:5-417:20 Type->Type 1573testdata/Builtins.lc 419:22-419:64 Type->Type
1575testdata/Builtins.lc 417:28-417:33 Type 1574testdata/Builtins.lc 419:22-420:99 Type
1576testdata/Builtins.lc 417:28-417:41 Type->Type 1575testdata/Builtins.lc 419:50-419:54 a:Type -> a -> a->Type
1577testdata/Builtins.lc 417:28-419:99 Type | Type->Type 1576testdata/Builtins.lc 419:50-419:58 Nat -> Nat->Type
1578testdata/Builtins.lc 417:37-417:41 Nat -> Type->Type | Type | Type->Type 1577testdata/Builtins.lc 419:50-419:61 Nat->Type
1579testdata/Builtins.lc 418:22-418:46 Type 1578testdata/Builtins.lc 419:50-419:64 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type
1580testdata/Builtins.lc 418:22-418:64 Type->Type 1579testdata/Builtins.lc 419:55-419:58 Type
1581testdata/Builtins.lc 418:22-419:99 Type 1580testdata/Builtins.lc 419:59-419:61 Nat
1582testdata/Builtins.lc 418:50-418:54 a:Type -> a -> a->Type 1581testdata/Builtins.lc 419:62-419:64 Nat
1583testdata/Builtins.lc 418:50-418:58 Nat -> Nat->Type 1582testdata/Builtins.lc 420:22-420:59 Type
1584testdata/Builtins.lc 418:50-418:61 Nat->Type 1583testdata/Builtins.lc 420:22-420:99 Type->Type
1585testdata/Builtins.lc 418:50-418:64 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type 1584testdata/Builtins.lc 420:63-420:65 Type -> Type->Type
1586testdata/Builtins.lc 418:55-418:58 Type 1585testdata/Builtins.lc 420:63-420:82 Type->Type
1587testdata/Builtins.lc 418:59-418:61 Nat 1586testdata/Builtins.lc 420:63-420:99 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type
1588testdata/Builtins.lc 418:62-418:64 Nat 1587testdata/Builtins.lc 420:66-420:82 Type
1589testdata/Builtins.lc 419:22-419:59 Type 1588testdata/Builtins.lc 420:67-420:71 a:Type -> a -> a->Type
1590testdata/Builtins.lc 419:22-419:99 Type->Type 1589testdata/Builtins.lc 420:67-420:75 Nat -> Nat->Type
1591testdata/Builtins.lc 419:63-419:65 Type -> Type->Type 1590testdata/Builtins.lc 420:67-420:78 Nat->Type
1592testdata/Builtins.lc 419:63-419:82 Type->Type 1591testdata/Builtins.lc 420:72-420:75 Type
1593testdata/Builtins.lc 419:63-419:99 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type 1592testdata/Builtins.lc 420:76-420:78 Nat
1594testdata/Builtins.lc 419:66-419:82 Type 1593testdata/Builtins.lc 420:79-420:81 Nat
1595testdata/Builtins.lc 419:67-419:71 a:Type -> a -> a->Type 1594testdata/Builtins.lc 420:83-420:99 Type
1596testdata/Builtins.lc 419:67-419:75 Nat -> Nat->Type 1595testdata/Builtins.lc 420:84-420:88 a:Type -> a -> a->Type
1597testdata/Builtins.lc 419:67-419:78 Nat->Type 1596testdata/Builtins.lc 420:84-420:92 Nat -> Nat->Type
1598testdata/Builtins.lc 419:72-419:75 Type 1597testdata/Builtins.lc 420:84-420:95 Nat->Type
1599testdata/Builtins.lc 419:76-419:78 Nat 1598testdata/Builtins.lc 420:89-420:92 Type
1600testdata/Builtins.lc 419:79-419:81 Nat 1599testdata/Builtins.lc 420:93-420:95 Nat
1601testdata/Builtins.lc 419:83-419:99 Type 1600testdata/Builtins.lc 420:96-420:98 Nat
1602testdata/Builtins.lc 419:84-419:88 a:Type -> a -> a->Type 1601testdata/Builtins.lc 422:7-422:20 Type->Type
1603testdata/Builtins.lc 419:84-419:92 Nat -> Nat->Type 1602testdata/Builtins.lc 422:7-422:65 Type
1604testdata/Builtins.lc 419:84-419:95 Nat->Type 1603testdata/Builtins.lc 422:29-422:42 {a} -> {b} -> {c : DefaultFragOp b} -> FragmentOperation b
1605testdata/Builtins.lc 419:89-419:92 Type 1604testdata/Builtins.lc 422:46-422:63 Type->Type
1606testdata/Builtins.lc 419:93-419:95 Nat 1605testdata/Builtins.lc 422:46-422:65 Type
1607testdata/Builtins.lc 419:96-419:98 Nat 1606testdata/Builtins.lc 422:64-422:65 Type
1608testdata/Builtins.lc 421:7-421:20 Type->Type 1607testdata/Builtins.lc 423:37-423:42 Type
1609testdata/Builtins.lc 421:7-421:65 Type 1608testdata/Builtins.lc 423:37-423:112 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3
1610testdata/Builtins.lc 421:29-421:42 {a} -> {b} -> {c : DefaultFragOp b} -> FragmentOperation b 1609testdata/Builtins.lc 423:37-424:36 Type | Type->Type
1611testdata/Builtins.lc 421:46-421:63 Type->Type 1610testdata/Builtins.lc 423:37-424:77 {a : DefaultFragOp V1} -> FragmentOperation V2 | {a} -> {b : DefaultFragOp a} -> FragmentOperation a
1612testdata/Builtins.lc 421:46-421:65 Type 1611testdata/Builtins.lc 423:69-423: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)
1613testdata/Builtins.lc 421:64-421:65 Type 1612testdata/Builtins.lc 423:69-423:87 VecScalar V2 Bool -> FragmentOperation (Color (VecScalar V3 V2))
1614testdata/Builtins.lc 422:37-422:42 Type 1613testdata/Builtins.lc 423:69-423:112 FragmentOperation (Color (VecS V1 4)) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a))))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ a)))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ a))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ a))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ a)))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ a)))} -> FragmentOperation (Color (VecS Float ('Succ a))) | a:Nat -> {b : DefaultFragOp (Color (VecS V1 a))} -> FragmentOperation (Color (VecS V2 a)) | a:Type -> b:Nat -> {c : DefaultFragOp (Color (VecS a b))} -> FragmentOperation (Color (VecS a b)) | a:Type -> {b : DefaultFragOp (Color a)} -> FragmentOperation (Color a)
1615testdata/Builtins.lc 422:37-422:112 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 1614testdata/Builtins.lc 423:77-423:87 {a} -> Blending a
1616testdata/Builtins.lc 422:37-423:36 Type | Type->Type 1615testdata/Builtins.lc 423:88-423:112 VecS Bool 4
1617testdata/Builtins.lc 422:37-423:77 {a : DefaultFragOp V1} -> FragmentOperation V2 | {a} -> {b : DefaultFragOp a} -> FragmentOperation a 1616testdata/Builtins.lc 423:89-423:91 {a} -> a -> a -> a -> a -> VecS a 4
1618testdata/Builtins.lc 422:69-422: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) 1617testdata/Builtins.lc 423:89-423:96 Bool -> Bool -> Bool -> VecS Bool 4
1619testdata/Builtins.lc 422:69-422:87 VecScalar V2 Bool -> FragmentOperation (Color (VecScalar V3 V2)) 1618testdata/Builtins.lc 423:89-423:101 Bool -> Bool -> VecS Bool 4
1620testdata/Builtins.lc 422:69-422:112 FragmentOperation (Color (VecS V1 4)) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a))))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ ('Succ a)))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ ('Succ a)))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ ('Succ a))))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ ('Succ a))))} -> FragmentOperation (Color (VecS Float ('Succ ('Succ a)))) | a:Nat -> {b : DefaultFragOp (Color (VecS Float ('Succ a)))} -> FragmentOperation (Color (VecS Float ('Succ a))) | a:Nat -> {b : DefaultFragOp (Color (VecS V1 a))} -> FragmentOperation (Color (VecS V2 a)) | a:Type -> b:Nat -> {c : DefaultFragOp (Color (VecS a b))} -> FragmentOperation (Color (VecS a b)) | a:Type -> {b : DefaultFragOp (Color a)} -> FragmentOperation (Color a) 1619testdata/Builtins.lc 423:89-423:106 Bool -> VecS Bool 4
1621testdata/Builtins.lc 422:77-422:87 {a} -> Blending a 1620testdata/Builtins.lc 423:92-423:96 Bool
1622testdata/Builtins.lc 422:88-422:112 VecS Bool 4 1621testdata/Builtins.lc 423:97-423:101 Bool
1623testdata/Builtins.lc 422:89-422:91 {a} -> a -> a -> a -> a -> VecS a 4 1622testdata/Builtins.lc 423:102-423:106 Bool
1624testdata/Builtins.lc 422:89-422:96 Bool -> Bool -> Bool -> VecS Bool 4 1623testdata/Builtins.lc 423:107-423:111 Bool
1625testdata/Builtins.lc 422:89-422:101 Bool -> Bool -> VecS Bool 4 1624testdata/Builtins.lc 424:31-424:36 Type
1626testdata/Builtins.lc 422:89-422:106 Bool -> VecS Bool 4 1625testdata/Builtins.lc 424:31-424:77 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3
1627testdata/Builtins.lc 422:92-422:96 Bool 1626testdata/Builtins.lc 424:60-424:67 ComparisonFunction -> Bool -> FragmentOperation (Depth Float)
1628testdata/Builtins.lc 422:97-422:101 Bool 1627testdata/Builtins.lc 424:60-424:72 Bool -> FragmentOperation (Depth Float)
1629testdata/Builtins.lc 422:102-422:106 Bool 1628testdata/Builtins.lc 424:60-424:77 FragmentOperation (Depth Float) | a:Type -> {b : DefaultFragOp (Depth a)} -> FragmentOperation (Depth a)
1630testdata/Builtins.lc 422:107-422:111 Bool 1629testdata/Builtins.lc 424:68-424:72 ComparisonFunction
1631testdata/Builtins.lc 423:31-423:36 Type 1630testdata/Builtins.lc 424:73-424:77 Bool
1632testdata/Builtins.lc 423:31-423:77 ({a : DefaultFragOp V1} -> FragmentOperation V2) -> {c : DefaultFragOp V2} -> FragmentOperation V3 1631testdata/Builtins.lc 431:6-431:17 Nat -> Type->Type | Type
1633testdata/Builtins.lc 423:60-423:67 ComparisonFunction -> Bool -> FragmentOperation (Depth Float) 1632testdata/Builtins.lc 431:24-431:27 Type
1634testdata/Builtins.lc 423:60-423:72 Bool -> FragmentOperation (Depth Float) 1633testdata/Builtins.lc 432:1-432:11 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a
1635testdata/Builtins.lc 423:60-423:77 FragmentOperation (Depth Float) | a:Type -> {b : DefaultFragOp (Depth a)} -> FragmentOperation (Depth a) 1634testdata/Builtins.lc 432:15-432:22 Type->Type
1636testdata/Builtins.lc 423:68-423:72 ComparisonFunction 1635testdata/Builtins.lc 432:15-432:24 Type
1637testdata/Builtins.lc 423:73-423:77 Bool 1636testdata/Builtins.lc 432:15-432:99 Type
1638testdata/Builtins.lc 430:6-430:17 Nat -> Type->Type | Type 1637testdata/Builtins.lc 432:23-432:24 V3
1639testdata/Builtins.lc 430:6-431:13 Type 1638testdata/Builtins.lc 432:28-432:42 Nat -> Type->Type
1640testdata/Builtins.lc 430:24-430:27 Type 1639testdata/Builtins.lc 432:28-432:44 Type->Type
1641testdata/Builtins.lc 431:3-431:13 FrameBuffer V5 V4 | Type | {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b 1640testdata/Builtins.lc 432:28-432:61 Type
1642testdata/Builtins.lc 431:19-431:27 Type->Type 1641testdata/Builtins.lc 432:28-432:99 Type
1643testdata/Builtins.lc 431:19-431:29 Type 1642testdata/Builtins.lc 432:43-432:44 V2
1644testdata/Builtins.lc 431:19-431:104 Type 1643testdata/Builtins.lc 432:45-432:61 Type
1645testdata/Builtins.lc 431:28-431:29 Type 1644testdata/Builtins.lc 432:46-432:58 Type->Type
1646testdata/Builtins.lc 431:33-431:47 Nat -> Type->Type 1645testdata/Builtins.lc 432:59-432:60 Type
1647testdata/Builtins.lc 431:33-431:49 Type->Type 1646testdata/Builtins.lc 432:65-432:76 Nat -> Type->Type
1648testdata/Builtins.lc 431:33-431:66 Type 1647testdata/Builtins.lc 432:65-432:78 Type->Type
1649testdata/Builtins.lc 431:33-431:104 Type 1648testdata/Builtins.lc 432:65-432:80 Type
1650testdata/Builtins.lc 431:48-431:49 Nat 1649testdata/Builtins.lc 432:65-432:99 Type
1651testdata/Builtins.lc 431:50-431:66 Type 1650testdata/Builtins.lc 432:77-432:78 Nat
1652testdata/Builtins.lc 431:51-431:63 Type->Type 1651testdata/Builtins.lc 432:79-432:80 Type
1653testdata/Builtins.lc 431:64-431:65 Type 1652testdata/Builtins.lc 432:84-432:95 Nat -> Type->Type
1654testdata/Builtins.lc 431:70-431:81 Nat -> Type->Type 1653testdata/Builtins.lc 432:84-432:97 Type->Type
1655testdata/Builtins.lc 431:70-431:83 Type->Type 1654testdata/Builtins.lc 432:84-432:99 Type
1656testdata/Builtins.lc 431:70-431:85 Type 1655testdata/Builtins.lc 432:96-432:97 Nat
1657testdata/Builtins.lc 431:70-431:104 Type 1656testdata/Builtins.lc 432:98-432:99 Type
1658testdata/Builtins.lc 431:82-431:83 Nat 1657testdata/Builtins.lc 435:5-435:18 Type->Type
1659testdata/Builtins.lc 431:84-431:85 Type 1658testdata/Builtins.lc 435:26-435:31 Type
1660testdata/Builtins.lc 431:89-431:100 Nat -> Type->Type 1659testdata/Builtins.lc 435:26-435:52 Type->Type
1661testdata/Builtins.lc 431:89-431:102 Type->Type 1660testdata/Builtins.lc 435:26-437:88 Type | Type->Type
1662testdata/Builtins.lc 431:89-431:104 Type 1661testdata/Builtins.lc 435:35-435:46 Nat -> Type->Type
1663testdata/Builtins.lc 431:101-431:102 Nat 1662testdata/Builtins.lc 435:35-435:49 Type->Type
1664testdata/Builtins.lc 431:103-431:104 Type 1663testdata/Builtins.lc 435:35-435:52 Nat -> Type->Type | Type | Type->Type
1665testdata/Builtins.lc 434:5-434:18 Type->Type 1664testdata/Builtins.lc 435:47-435:49 Nat
1666testdata/Builtins.lc 434:26-434:31 Type 1665testdata/Builtins.lc 435:50-435:52 Type
1667testdata/Builtins.lc 434:26-434:52 Type->Type 1666testdata/Builtins.lc 436:20-436:44 Type
1668testdata/Builtins.lc 434:26-436:88 Type | Type->Type 1667testdata/Builtins.lc 436:20-436:71 Type->Type
1669testdata/Builtins.lc 434:35-434:46 Nat -> Type->Type 1668testdata/Builtins.lc 436:20-437:88 Type
1670testdata/Builtins.lc 434:35-434:49 Type->Type 1669testdata/Builtins.lc 436:48-436:59 Nat -> Type->Type
1671testdata/Builtins.lc 434:35-434:52 Nat -> Type->Type | Type | Type->Type 1670testdata/Builtins.lc 436:48-436:62 Type->Type
1672testdata/Builtins.lc 434:47-434:49 Nat 1671testdata/Builtins.lc 436:48-436:71 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type
1673testdata/Builtins.lc 434:50-434:52 Type 1672testdata/Builtins.lc 436:60-436:62 Nat
1674testdata/Builtins.lc 435:20-435:44 Type 1673testdata/Builtins.lc 436:63-436:71 Type
1675testdata/Builtins.lc 435:20-435:71 Type->Type 1674testdata/Builtins.lc 436:64-436:66 Type
1676testdata/Builtins.lc 435:20-436:88 Type 1675testdata/Builtins.lc 436:68-436:70 Type
1677testdata/Builtins.lc 435:48-435:59 Nat -> Type->Type 1676testdata/Builtins.lc 437:20-437:57 Type
1678testdata/Builtins.lc 435:48-435:62 Type->Type 1677testdata/Builtins.lc 437:20-437:88 Type->Type
1679testdata/Builtins.lc 435:48-435:71 Nat -> Type->Type | Type | Type -> Type->Type | Type->Type 1678testdata/Builtins.lc 437:61-437:72 Nat -> Type->Type
1680testdata/Builtins.lc 435:60-435:62 Nat 1679testdata/Builtins.lc 437:61-437:75 Type->Type
1681testdata/Builtins.lc 435:63-435:71 Type 1680testdata/Builtins.lc 437:61-437:88 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type
1682testdata/Builtins.lc 435:64-435:66 Type 1681testdata/Builtins.lc 437:73-437:75 Nat
1683testdata/Builtins.lc 435:68-435:70 Type 1682testdata/Builtins.lc 437:76-437:88 Type
1684testdata/Builtins.lc 436:20-436:57 Type 1683testdata/Builtins.lc 437:77-437:79 Type
1685testdata/Builtins.lc 436:20-436:88 Type->Type 1684testdata/Builtins.lc 437:77-437:83 Type->Type
1686testdata/Builtins.lc 436:61-436:72 Nat -> Type->Type 1685testdata/Builtins.lc 437:81-437:83 Type
1687testdata/Builtins.lc 436:61-436:75 Type->Type 1686testdata/Builtins.lc 437:85-437:87 Type
1688testdata/Builtins.lc 436:61-436:88 Nat -> Type->Type | Type | Type -> Type -> Type->Type | Type -> Type->Type | Type->Type 1687testdata/Builtins.lc 439:1-439:12 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a
1689testdata/Builtins.lc 436:73-436:75 Nat 1688testdata/Builtins.lc 439:17-439:115 Type
1690testdata/Builtins.lc 436:76-436:88 Type 1689testdata/Builtins.lc 439:18-439:34 Type->Type
1691testdata/Builtins.lc 436:77-436:79 Type 1690testdata/Builtins.lc 439:18-439:36 Type
1692testdata/Builtins.lc 436:77-436:83 Type->Type 1691testdata/Builtins.lc 439:35-439:36 V5
1693testdata/Builtins.lc 436:81-436:83 Type 1692testdata/Builtins.lc 439:38-439:53 Type->Type
1694testdata/Builtins.lc 436:85-436:87 Type 1693testdata/Builtins.lc 439:38-439:55 Type
1695testdata/Builtins.lc 438:1-438:12 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a 1694testdata/Builtins.lc 439:38-439:115 Type
1696testdata/Builtins.lc 438:17-438:115 Type 1695testdata/Builtins.lc 439:54-439:55 V4
1697testdata/Builtins.lc 438:18-438:34 Type->Type 1696testdata/Builtins.lc 439:57-439:68 Nat -> Type->Type
1698testdata/Builtins.lc 438:18-438:36 Type 1697testdata/Builtins.lc 439:57-439:70 Type->Type
1699testdata/Builtins.lc 438:35-438:36 V5 1698testdata/Builtins.lc 439:57-439:72 Type
1700testdata/Builtins.lc 438:38-438:53 Type->Type 1699testdata/Builtins.lc 439:57-439:74 Type->Type
1701testdata/Builtins.lc 438:38-438:55 Type 1700testdata/Builtins.lc 439:57-439:90 Type
1702testdata/Builtins.lc 438:38-438:115 Type 1701testdata/Builtins.lc 439:57-439:115 Type
1703testdata/Builtins.lc 438:54-438:55 V4 1702testdata/Builtins.lc 439:69-439:70 V3
1704testdata/Builtins.lc 438:57-438:68 Nat -> Type->Type 1703testdata/Builtins.lc 439:71-439:72 Type
1705testdata/Builtins.lc 438:57-438:70 Type->Type 1704testdata/Builtins.lc 439:73-439:74 Type -> Type->Type
1706testdata/Builtins.lc 438:57-438:72 Type 1705testdata/Builtins.lc 439:75-439:88 Type->Type
1707testdata/Builtins.lc 438:57-438:74 Type->Type 1706testdata/Builtins.lc 439:75-439:90 Type
1708testdata/Builtins.lc 438:57-438:90 Type 1707testdata/Builtins.lc 439:89-439:90 Type
1709testdata/Builtins.lc 438:57-438:115 Type 1708testdata/Builtins.lc 439:95-439:96 Type
1710testdata/Builtins.lc 438:69-438:70 V3 1709testdata/Builtins.lc 439:95-439:115 Type
1711testdata/Builtins.lc 438:71-438:72 Type 1710testdata/Builtins.lc 439:100-439:111 Nat -> Type->Type
1712testdata/Builtins.lc 438:73-438:74 Type -> Type->Type 1711testdata/Builtins.lc 439:100-439:113 Type->Type
1713testdata/Builtins.lc 438:75-438:88 Type->Type 1712testdata/Builtins.lc 439:100-439:115 Type
1714testdata/Builtins.lc 438:75-438:90 Type 1713testdata/Builtins.lc 439:112-439:113 Nat
1715testdata/Builtins.lc 438:89-438:90 Type 1714testdata/Builtins.lc 439:114-439:115 Type
1716testdata/Builtins.lc 438:95-438:96 Type 1715testdata/Builtins.lc 441:1-441:11 {a} -> {b:Nat} -> {c} -> FragOps a -> (c -> RemSemantics a) -> List (Vector b (Maybe (SimpleFragment c))) -> FrameBuffer b a -> FrameBuffer b a
1717testdata/Builtins.lc 438:95-438:115 Type 1716testdata/Builtins.lc 441:34-441:44 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a
1718testdata/Builtins.lc 438:100-438:111 Nat -> Type->Type 1717testdata/Builtins.lc 441:34-441:48 List (Vector V0 (Maybe (SimpleFragment (RemSemantics V1)))) -> FrameBuffer V1 V2 -> FrameBuffer V2 V3
1719testdata/Builtins.lc 438:100-438:113 Type->Type 1718testdata/Builtins.lc 441:34-441:76 FrameBuffer V1 V2 -> FrameBuffer V2 V3
1720testdata/Builtins.lc 438:100-438:115 Type 1719testdata/Builtins.lc 441:34-441:79 FrameBuffer V1 V2
1721testdata/Builtins.lc 438:112-438:113 Nat 1720testdata/Builtins.lc 441:45-441:48 V9
1722testdata/Builtins.lc 438:114-438:115 Type 1721testdata/Builtins.lc 441:49-441:76 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V2))))
1723testdata/Builtins.lc 440:1-440:11 {a:Nat} -> {b} -> {c} -> FragOps' b -> (c -> RemSemantics b) -> List (Vector a (Maybe (SimpleFragment c))) -> FrameBuffer a b -> FrameBuffer a b 1722testdata/Builtins.lc 441:50-441:62 {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b)))
1724testdata/Builtins.lc 440:34-440:44 {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b 1723testdata/Builtins.lc 441:50-441:70 List (Vector V0 (Maybe (SimpleFragment V2))) -> List (Vector V1 (Maybe (SimpleFragment V2)))
1725testdata/Builtins.lc 440:34-440:48 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V0)))) -> FrameBuffer V2 V1 -> FrameBuffer V3 V2 1724testdata/Builtins.lc 441:63-441:70 V10
1726testdata/Builtins.lc 440:34-440:76 FrameBuffer V2 V1 -> FrameBuffer V3 V2 1725testdata/Builtins.lc 441:71-441:75 V6
1727testdata/Builtins.lc 440:34-440:79 FrameBuffer V2 V1 1726testdata/Builtins.lc 441:77-441:79 V4
1728testdata/Builtins.lc 440:45-440:48 V9 1727testdata/Builtins.lc 443:1-443:20 {a} -> a->a
1729testdata/Builtins.lc 440:49-440:76 List (Vector V2 (Maybe (SimpleFragment (RemSemantics V1)))) 1728testdata/Builtins.lc 443:25-443:26 V1
1730testdata/Builtins.lc 440:50-440:62 {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b))) 1729testdata/Builtins.lc 446:1-446:9 {a} -> FrameBuffer 1 a -> Image 1 a
1731testdata/Builtins.lc 440:50-440:70 List (Vector V0 (Maybe (SimpleFragment V2))) -> List (Vector V1 (Maybe (SimpleFragment V2)))
1732testdata/Builtins.lc 440:63-440:70 V10
1733testdata/Builtins.lc 440:71-440:75 V6
1734testdata/Builtins.lc 440:77-440:79 V4
1735testdata/Builtins.lc 442:1-442:20 {a} -> a->a
1736testdata/Builtins.lc 442:25-442:26 V1
1737testdata/Builtins.lc 445:1-445:9 {a} -> FrameBuffer 1 a -> Image 1 a
1738testdata/Builtins.lc 445:24-445:35 Nat -> Type->Type
1739testdata/Builtins.lc 445:24-445:37 Type->Type
1740testdata/Builtins.lc 445:24-445:39 Type
1741testdata/Builtins.lc 445:24-445:52 Type
1742testdata/Builtins.lc 445:36-445:37 V1
1743testdata/Builtins.lc 445:38-445:39 V1
1744testdata/Builtins.lc 445:43-445:48 Nat -> Type->Type
1745testdata/Builtins.lc 445:43-445:50 Type->Type
1746testdata/Builtins.lc 445:43-445:52 Type
1747testdata/Builtins.lc 445:49-445:50 V1
1748testdata/Builtins.lc 445:51-445:52 Type
1749testdata/Builtins.lc 446:1-446:14 FrameBuffer 1 (Tuple2 (Depth Float) (Color (VecS Float 4))) -> Image 1 (Color (VecS Float 4))
1750testdata/Builtins.lc 446:24-446:35 Nat -> Type->Type 1730testdata/Builtins.lc 446:24-446:35 Nat -> Type->Type
1751testdata/Builtins.lc 446:24-446:37 Type->Type 1731testdata/Builtins.lc 446:24-446:37 Type->Type
1752testdata/Builtins.lc 446:24-446:72 Type 1732testdata/Builtins.lc 446:24-446:39 Type
1733testdata/Builtins.lc 446:24-446:52 Type
1753testdata/Builtins.lc 446:36-446:37 V1 1734testdata/Builtins.lc 446:36-446:37 V1
1754testdata/Builtins.lc 446:38-446:72 Type 1735testdata/Builtins.lc 446:38-446:39 V1
1755testdata/Builtins.lc 446:39-446:44 Type->Type 1736testdata/Builtins.lc 446:43-446:48 Nat -> Type->Type
1756testdata/Builtins.lc 446:39-446:50 Type 1737testdata/Builtins.lc 446:43-446:50 Type->Type
1757testdata/Builtins.lc 446:45-446:50 Type 1738testdata/Builtins.lc 446:43-446:52 Type
1758testdata/Builtins.lc 446:52-446:57 Type->Type 1739testdata/Builtins.lc 446:49-446:50 V1
1759testdata/Builtins.lc 446:52-446:71 Type 1740testdata/Builtins.lc 446:51-446:52 Type
1760testdata/Builtins.lc 446:58-446:71 Type 1741testdata/Builtins.lc 447:1-447:14 FrameBuffer 1 (Tuple2 (Depth Float) (Color (VecS Float 4))) -> Image 1 (Color (VecS Float 4))
1761testdata/Builtins.lc 446:59-446:62 Nat -> Type->Type 1742testdata/Builtins.lc 447:24-447:35 Nat -> Type->Type
1762testdata/Builtins.lc 446:59-446:64 Type->Type 1743testdata/Builtins.lc 447:24-447:37 Type->Type
1763testdata/Builtins.lc 446:63-446:64 V1 1744testdata/Builtins.lc 447:24-447:72 Type
1764testdata/Builtins.lc 446:65-446:70 Type 1745testdata/Builtins.lc 447:36-447:37 V1
1765testdata/Builtins.lc 446:76-446:81 Nat -> Type->Type 1746testdata/Builtins.lc 447:38-447:72 Type
1766testdata/Builtins.lc 446:76-446:83 Type->Type 1747testdata/Builtins.lc 447:39-447:44 Type->Type
1767testdata/Builtins.lc 446:76-446:105 Type 1748testdata/Builtins.lc 447:39-447:50 Type
1768testdata/Builtins.lc 446:82-446:83 V1 1749testdata/Builtins.lc 447:45-447:50 Type
1769testdata/Builtins.lc 446:84-446:105 Type 1750testdata/Builtins.lc 447:52-447:57 Type->Type
1770testdata/Builtins.lc 446:85-446:90 Type->Type 1751testdata/Builtins.lc 447:52-447:71 Type
1771testdata/Builtins.lc 446:91-446:104 Type 1752testdata/Builtins.lc 447:58-447:71 Type
1772testdata/Builtins.lc 446:92-446:95 Nat -> Type->Type 1753testdata/Builtins.lc 447:59-447:62 Nat -> Type->Type
1773testdata/Builtins.lc 446:92-446:97 Type->Type 1754testdata/Builtins.lc 447:59-447:64 Type->Type
1774testdata/Builtins.lc 446:96-446:97 V1 1755testdata/Builtins.lc 447:63-447:64 V1
1775testdata/Builtins.lc 446:98-446:103 Type 1756testdata/Builtins.lc 447:65-447:70 Type
1776testdata/Builtins.lc 448:6-448:12 Type 1757testdata/Builtins.lc 447:76-447:81 Nat -> Type->Type
1777testdata/Builtins.lc 448:6-449:12 Type 1758testdata/Builtins.lc 447:76-447:83 Type->Type
1778testdata/Builtins.lc 449:3-449:12 Output | Type | {a:Nat} -> {b} -> FrameBuffer a b -> Output 1759testdata/Builtins.lc 447:76-447:105 Type
1779testdata/Builtins.lc 449:26-449:37 Nat -> Type->Type 1760testdata/Builtins.lc 447:82-447:83 V1
1780testdata/Builtins.lc 449:26-449:39 Type->Type 1761testdata/Builtins.lc 447:84-447:105 Type
1781testdata/Builtins.lc 449:26-449:41 Type 1762testdata/Builtins.lc 447:85-447:90 Type->Type
1782testdata/Builtins.lc 449:26-449:51 Type 1763testdata/Builtins.lc 447:91-447:104 Type
1783testdata/Builtins.lc 449:38-449:39 V3 1764testdata/Builtins.lc 447:92-447:95 Nat -> Type->Type
1784testdata/Builtins.lc 449:40-449:41 V1 1765testdata/Builtins.lc 447:92-447:97 Type->Type
1785testdata/Builtins.lc 449:45-449:51 Type 1766testdata/Builtins.lc 447:96-447:97 V1
1786testdata/Builtins.lc 455:1-455:8 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a 1767testdata/Builtins.lc 447:98-447:103 Type
1787testdata/Builtins.lc 455:10-455:17 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a 1768testdata/Builtins.lc 449:6-449:12 Type
1788testdata/Builtins.lc 455:19-455:26 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a 1769testdata/Builtins.lc 449:6-450:12 Type
1789testdata/Builtins.lc 455:34-455:37 Type->Type 1770testdata/Builtins.lc 450:3-450:12 Output | Type | {a:Nat} -> {b} -> FrameBuffer a b -> Output
1790testdata/Builtins.lc 455:34-455:58 Type 1771testdata/Builtins.lc 450:26-450:37 Nat -> Type->Type
1791testdata/Builtins.lc 455:34-455:73 Type 1772testdata/Builtins.lc 450:26-450:39 Type->Type
1792testdata/Builtins.lc 455:38-455:58 Type 1773testdata/Builtins.lc 450:26-450:41 Type
1793testdata/Builtins.lc 455:39-455:55 Type->Type 1774testdata/Builtins.lc 450:26-450:51 Type
1794testdata/Builtins.lc 455:56-455:57 V1 1775testdata/Builtins.lc 450:38-450:39 V3
1795testdata/Builtins.lc 455:62-455:63 Type 1776testdata/Builtins.lc 450:40-450:41 V1
1796testdata/Builtins.lc 455:62-455:73 Type 1777testdata/Builtins.lc 450:45-450:51 Type
1797testdata/Builtins.lc 455:67-455:68 Type 1778testdata/Builtins.lc 456:1-456:8 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
1798testdata/Builtins.lc 455:67-455:73 Type 1779testdata/Builtins.lc 456:10-456:17 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
1799testdata/Builtins.lc 455:72-455:73 Type 1780testdata/Builtins.lc 456:19-456:26 {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
1800testdata/Builtins.lc 456:1-456:9 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b 1781testdata/Builtins.lc 456:34-456:37 Type->Type
1801testdata/Builtins.lc 456:11-456:19 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b 1782testdata/Builtins.lc 456:34-456:58 Type
1802testdata/Builtins.lc 456:21-456:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b 1783testdata/Builtins.lc 456:34-456:73 Type
1803testdata/Builtins.lc 456:34-456:80 Type 1784testdata/Builtins.lc 456:38-456:58 Type
1804testdata/Builtins.lc 456:35-456:36 V3
1805testdata/Builtins.lc 456:35-456:38 Type->Type
1806testdata/Builtins.lc 456:35-456:57 Type
1807testdata/Builtins.lc 456:37-456:38 Type -> Type->Type
1808testdata/Builtins.lc 456:39-456:55 Type->Type 1785testdata/Builtins.lc 456:39-456:55 Type->Type
1809testdata/Builtins.lc 456:39-456:57 Type
1810testdata/Builtins.lc 456:56-456:57 V1 1786testdata/Builtins.lc 456:56-456:57 V1
1811testdata/Builtins.lc 456:59-456:62 Type->Type 1787testdata/Builtins.lc 456:62-456:63 Type
1812testdata/Builtins.lc 456:59-456:64 Type 1788testdata/Builtins.lc 456:62-456:73 Type
1813testdata/Builtins.lc 456:59-456:80 Type 1789testdata/Builtins.lc 456:67-456:68 Type
1814testdata/Builtins.lc 456:63-456:64 Type 1790testdata/Builtins.lc 456:67-456:73 Type
1815testdata/Builtins.lc 456:69-456:70 Type 1791testdata/Builtins.lc 456:72-456:73 Type
1816testdata/Builtins.lc 456:69-456:80 Type 1792testdata/Builtins.lc 457:1-457:9 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
1817testdata/Builtins.lc 456:74-456:75 Type 1793testdata/Builtins.lc 457:11-457:19 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
1818testdata/Builtins.lc 456:74-456:80 Type 1794testdata/Builtins.lc 457:21-457:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
1819testdata/Builtins.lc 456:79-456:80 Type 1795testdata/Builtins.lc 457:34-457:80 Type
1820testdata/Builtins.lc 457:1-457:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b 1796testdata/Builtins.lc 457:35-457:36 V3
1821testdata/Builtins.lc 457:10-457:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
1822testdata/Builtins.lc 457:34-457:75 Type
1823testdata/Builtins.lc 457:35-457:38 Type->Type 1797testdata/Builtins.lc 457:35-457:38 Type->Type
1824testdata/Builtins.lc 457:35-457:40 Type 1798testdata/Builtins.lc 457:35-457:57 Type
1825testdata/Builtins.lc 457:39-457:40 V5 1799testdata/Builtins.lc 457:37-457:38 Type -> Type->Type
1826testdata/Builtins.lc 457:42-457:43 V4 1800testdata/Builtins.lc 457:39-457:55 Type->Type
1827testdata/Builtins.lc 457:42-457:45 Type->Type 1801testdata/Builtins.lc 457:39-457:57 Type
1828testdata/Builtins.lc 457:42-457:59 Type 1802testdata/Builtins.lc 457:56-457:57 V1
1829testdata/Builtins.lc 457:42-457:75 Type 1803testdata/Builtins.lc 457:59-457:62 Type->Type
1830testdata/Builtins.lc 457:44-457:45 Type -> Type->Type 1804testdata/Builtins.lc 457:59-457:64 Type
1831testdata/Builtins.lc 457:46-457:55 Nat -> Type->Type 1805testdata/Builtins.lc 457:59-457:80 Type
1832testdata/Builtins.lc 457:46-457:57 Type->Type 1806testdata/Builtins.lc 457:63-457:64 Type
1833testdata/Builtins.lc 457:46-457:59 Type
1834testdata/Builtins.lc 457:56-457:57 V2
1835testdata/Builtins.lc 457:58-457:59 Type
1836testdata/Builtins.lc 457:64-457:65 Type
1837testdata/Builtins.lc 457:64-457:75 Type
1838testdata/Builtins.lc 457:69-457:70 Type 1807testdata/Builtins.lc 457:69-457:70 Type
1839testdata/Builtins.lc 457:69-457:75 Type 1808testdata/Builtins.lc 457:69-457:80 Type
1840testdata/Builtins.lc 457:74-457:75 Type 1809testdata/Builtins.lc 457:74-457:75 Type
1841testdata/Builtins.lc 458:1-458:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b 1810testdata/Builtins.lc 457:74-457:80 Type
1842testdata/Builtins.lc 458:11-458:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b 1811testdata/Builtins.lc 457:79-457:80 Type
1812testdata/Builtins.lc 458:1-458:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
1813testdata/Builtins.lc 458:10-458:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
1843testdata/Builtins.lc 458:34-458:75 Type 1814testdata/Builtins.lc 458:34-458:75 Type
1844testdata/Builtins.lc 458:35-458:38 Type->Type 1815testdata/Builtins.lc 458:35-458:38 Type->Type
1845testdata/Builtins.lc 458:35-458:40 Type 1816testdata/Builtins.lc 458:35-458:40 Type
@@ -1859,41 +1830,40 @@ testdata/Builtins.lc 458:64-458:75 Type
1859testdata/Builtins.lc 458:69-458:70 Type 1830testdata/Builtins.lc 458:69-458:70 Type
1860testdata/Builtins.lc 458:69-458:75 Type 1831testdata/Builtins.lc 458:69-458:75 Type
1861testdata/Builtins.lc 458:74-458:75 Type 1832testdata/Builtins.lc 458:74-458:75 Type
1862testdata/Builtins.lc 459:1-459:8 {a} -> {b : Signed (MatVecScalarElem a)} -> a->a 1833testdata/Builtins.lc 459:1-459:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
1863testdata/Builtins.lc 459:34-459:40 Type->Type 1834testdata/Builtins.lc 459:11-459:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
1864testdata/Builtins.lc 459:34-459:61 Type 1835testdata/Builtins.lc 459:34-459:75 Type
1865testdata/Builtins.lc 459:34-459:71 Type 1836testdata/Builtins.lc 459:35-459:38 Type->Type
1866testdata/Builtins.lc 459:41-459:61 Type 1837testdata/Builtins.lc 459:35-459:40 Type
1867testdata/Builtins.lc 459:42-459:58 Type->Type 1838testdata/Builtins.lc 459:39-459:40 V5
1868testdata/Builtins.lc 459:59-459:60 V1 1839testdata/Builtins.lc 459:42-459:43 V4
1869testdata/Builtins.lc 459:65-459:66 Type 1840testdata/Builtins.lc 459:42-459:45 Type->Type
1870testdata/Builtins.lc 459:65-459:71 Type 1841testdata/Builtins.lc 459:42-459:59 Type
1871testdata/Builtins.lc 459:70-459:71 Type 1842testdata/Builtins.lc 459:42-459:75 Type
1872testdata/Builtins.lc 461:1-461:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b 1843testdata/Builtins.lc 459:44-459:45 Type -> Type->Type
1873testdata/Builtins.lc 461:11-461:18 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b 1844testdata/Builtins.lc 459:46-459:55 Nat -> Type->Type
1874testdata/Builtins.lc 461:20-461:28 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b 1845testdata/Builtins.lc 459:46-459:57 Type->Type
1875testdata/Builtins.lc 461:34-461:80 Type 1846testdata/Builtins.lc 459:46-459:59 Type
1876testdata/Builtins.lc 461:35-461:43 Type->Type 1847testdata/Builtins.lc 459:56-459:57 V2
1877testdata/Builtins.lc 461:35-461:45 Type 1848testdata/Builtins.lc 459:58-459:59 Type
1878testdata/Builtins.lc 461:44-461:45 V5 1849testdata/Builtins.lc 459:64-459:65 Type
1879testdata/Builtins.lc 461:47-461:48 V4 1850testdata/Builtins.lc 459:64-459:75 Type
1880testdata/Builtins.lc 461:47-461:50 Type->Type 1851testdata/Builtins.lc 459:69-459:70 Type
1881testdata/Builtins.lc 461:47-461:64 Type 1852testdata/Builtins.lc 459:69-459:75 Type
1882testdata/Builtins.lc 461:47-461:80 Type 1853testdata/Builtins.lc 459:74-459:75 Type
1883testdata/Builtins.lc 461:49-461:50 Type -> Type->Type 1854testdata/Builtins.lc 460:1-460:8 {a} -> {b : Signed (MatVecScalarElem a)} -> a->a
1884testdata/Builtins.lc 461:51-461:60 Nat -> Type->Type 1855testdata/Builtins.lc 460:34-460:40 Type->Type
1885testdata/Builtins.lc 461:51-461:62 Type->Type 1856testdata/Builtins.lc 460:34-460:61 Type
1886testdata/Builtins.lc 461:51-461:64 Type 1857testdata/Builtins.lc 460:34-460:71 Type
1887testdata/Builtins.lc 461:61-461:62 V2 1858testdata/Builtins.lc 460:41-460:61 Type
1888testdata/Builtins.lc 461:63-461:64 Type 1859testdata/Builtins.lc 460:42-460:58 Type->Type
1889testdata/Builtins.lc 461:69-461:70 Type 1860testdata/Builtins.lc 460:59-460:60 V1
1890testdata/Builtins.lc 461:69-461:80 Type 1861testdata/Builtins.lc 460:65-460:66 Type
1891testdata/Builtins.lc 461:74-461:75 Type 1862testdata/Builtins.lc 460:65-460:71 Type
1892testdata/Builtins.lc 461:74-461:80 Type 1863testdata/Builtins.lc 460:70-460:71 Type
1893testdata/Builtins.lc 461:79-461:80 Type 1864testdata/Builtins.lc 462:1-462:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
1894testdata/Builtins.lc 462:1-462:10 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b 1865testdata/Builtins.lc 462:11-462:18 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
1895testdata/Builtins.lc 462:12-462:20 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b 1866testdata/Builtins.lc 462:20-462:28 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
1896testdata/Builtins.lc 462:22-462:31 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
1897testdata/Builtins.lc 462:34-462:80 Type 1867testdata/Builtins.lc 462:34-462:80 Type
1898testdata/Builtins.lc 462:35-462:43 Type->Type 1868testdata/Builtins.lc 462:35-462:43 Type->Type
1899testdata/Builtins.lc 462:35-462:45 Type 1869testdata/Builtins.lc 462:35-462:45 Type
@@ -1913,15 +1883,17 @@ testdata/Builtins.lc 462:69-462:80 Type
1913testdata/Builtins.lc 462:74-462:75 Type 1883testdata/Builtins.lc 462:74-462:75 Type
1914testdata/Builtins.lc 462:74-462:80 Type 1884testdata/Builtins.lc 462:74-462:80 Type
1915testdata/Builtins.lc 462:79-462:80 Type 1885testdata/Builtins.lc 462:79-462:80 Type
1916testdata/Builtins.lc 463:1-463:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b->b 1886testdata/Builtins.lc 463:1-463:10 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
1917testdata/Builtins.lc 463:34-463:75 Type 1887testdata/Builtins.lc 463:12-463:20 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
1888testdata/Builtins.lc 463:22-463:31 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
1889testdata/Builtins.lc 463:34-463:80 Type
1918testdata/Builtins.lc 463:35-463:43 Type->Type 1890testdata/Builtins.lc 463:35-463:43 Type->Type
1919testdata/Builtins.lc 463:35-463:45 Type 1891testdata/Builtins.lc 463:35-463:45 Type
1920testdata/Builtins.lc 463:44-463:45 V5 1892testdata/Builtins.lc 463:44-463:45 V5
1921testdata/Builtins.lc 463:47-463:48 V4 1893testdata/Builtins.lc 463:47-463:48 V4
1922testdata/Builtins.lc 463:47-463:50 Type->Type 1894testdata/Builtins.lc 463:47-463:50 Type->Type
1923testdata/Builtins.lc 463:47-463:64 Type 1895testdata/Builtins.lc 463:47-463:64 Type
1924testdata/Builtins.lc 463:47-463:75 Type 1896testdata/Builtins.lc 463:47-463:80 Type
1925testdata/Builtins.lc 463:49-463:50 Type -> Type->Type 1897testdata/Builtins.lc 463:49-463:50 Type -> Type->Type
1926testdata/Builtins.lc 463:51-463:60 Nat -> Type->Type 1898testdata/Builtins.lc 463:51-463:60 Nat -> Type->Type
1927testdata/Builtins.lc 463:51-463:62 Type->Type 1899testdata/Builtins.lc 463:51-463:62 Type->Type
@@ -1929,127 +1901,132 @@ testdata/Builtins.lc 463:51-463:64 Type
1929testdata/Builtins.lc 463:61-463:62 V2 1901testdata/Builtins.lc 463:61-463:62 V2
1930testdata/Builtins.lc 463:63-463:64 Type 1902testdata/Builtins.lc 463:63-463:64 Type
1931testdata/Builtins.lc 463:69-463:70 Type 1903testdata/Builtins.lc 463:69-463:70 Type
1932testdata/Builtins.lc 463:69-463:75 Type 1904testdata/Builtins.lc 463:69-463:80 Type
1933testdata/Builtins.lc 463:74-463:75 Type 1905testdata/Builtins.lc 463:74-463:75 Type
1934testdata/Builtins.lc 464:1-464:12 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b 1906testdata/Builtins.lc 463:74-463:80 Type
1935testdata/Builtins.lc 464:14-464:25 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b 1907testdata/Builtins.lc 463:79-463:80 Type
1936testdata/Builtins.lc 464:34-464:102 Type 1908testdata/Builtins.lc 464:1-464:9 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b->b
1909testdata/Builtins.lc 464:34-464:75 Type
1937testdata/Builtins.lc 464:35-464:43 Type->Type 1910testdata/Builtins.lc 464:35-464:43 Type->Type
1938testdata/Builtins.lc 464:35-464:45 Type 1911testdata/Builtins.lc 464:35-464:45 Type
1939testdata/Builtins.lc 464:44-464:45 V7 1912testdata/Builtins.lc 464:44-464:45 V5
1940testdata/Builtins.lc 464:47-464:48 V6 1913testdata/Builtins.lc 464:47-464:48 V4
1941testdata/Builtins.lc 464:47-464:50 Type->Type 1914testdata/Builtins.lc 464:47-464:50 Type->Type
1942testdata/Builtins.lc 464:47-464:64 Type 1915testdata/Builtins.lc 464:47-464:64 Type
1943testdata/Builtins.lc 464:47-464:102 Type 1916testdata/Builtins.lc 464:47-464:75 Type
1944testdata/Builtins.lc 464:49-464:50 Type -> Type->Type 1917testdata/Builtins.lc 464:49-464:50 Type -> Type->Type
1945testdata/Builtins.lc 464:51-464:60 Nat -> Type->Type 1918testdata/Builtins.lc 464:51-464:60 Nat -> Type->Type
1946testdata/Builtins.lc 464:51-464:62 Type->Type 1919testdata/Builtins.lc 464:51-464:62 Type->Type
1947testdata/Builtins.lc 464:51-464:64 Type 1920testdata/Builtins.lc 464:51-464:64 Type
1948testdata/Builtins.lc 464:61-464:62 V4 1921testdata/Builtins.lc 464:61-464:62 V2
1949testdata/Builtins.lc 464:63-464:64 Type 1922testdata/Builtins.lc 464:63-464:64 Type
1950testdata/Builtins.lc 464:66-464:67 V3 1923testdata/Builtins.lc 464:69-464:70 Type
1951testdata/Builtins.lc 464:66-464:69 Type->Type 1924testdata/Builtins.lc 464:69-464:75 Type
1952testdata/Builtins.lc 464:66-464:86 Type 1925testdata/Builtins.lc 464:74-464:75 Type
1953testdata/Builtins.lc 464:66-464:102 Type 1926testdata/Builtins.lc 465:1-465:12 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b
1954testdata/Builtins.lc 464:68-464:69 Type -> Type->Type 1927testdata/Builtins.lc 465:14-465:25 {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b
1955testdata/Builtins.lc 464:70-464:79 Nat -> Type->Type 1928testdata/Builtins.lc 465:34-465:102 Type
1956testdata/Builtins.lc 464:70-464:81 Type->Type
1957testdata/Builtins.lc 464:70-464:86 Type
1958testdata/Builtins.lc 464:80-464:81 Nat
1959testdata/Builtins.lc 464:82-464:86 Type
1960testdata/Builtins.lc 464:91-464:92 Type
1961testdata/Builtins.lc 464:91-464:102 Type
1962testdata/Builtins.lc 464:96-464:97 Type
1963testdata/Builtins.lc 464:96-464:102 Type
1964testdata/Builtins.lc 464:101-464:102 Type
1965testdata/Builtins.lc 465:1-465:13 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
1966testdata/Builtins.lc 465:15-465:27 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
1967testdata/Builtins.lc 465:34-465:83 Type
1968testdata/Builtins.lc 465:35-465:43 Type->Type 1929testdata/Builtins.lc 465:35-465:43 Type->Type
1969testdata/Builtins.lc 465:35-465:45 Type 1930testdata/Builtins.lc 465:35-465:45 Type
1970testdata/Builtins.lc 465:44-465:45 V5 1931testdata/Builtins.lc 465:44-465:45 V7
1971testdata/Builtins.lc 465:47-465:48 V4 1932testdata/Builtins.lc 465:47-465:48 V6
1972testdata/Builtins.lc 465:47-465:50 Type->Type 1933testdata/Builtins.lc 465:47-465:50 Type->Type
1973testdata/Builtins.lc 465:47-465:64 Type 1934testdata/Builtins.lc 465:47-465:64 Type
1974testdata/Builtins.lc 465:47-465:83 Type 1935testdata/Builtins.lc 465:47-465:102 Type
1975testdata/Builtins.lc 465:49-465:50 Type -> Type->Type 1936testdata/Builtins.lc 465:49-465:50 Type -> Type->Type
1976testdata/Builtins.lc 465:51-465:60 Nat -> Type->Type 1937testdata/Builtins.lc 465:51-465:60 Nat -> Type->Type
1977testdata/Builtins.lc 465:51-465:62 Type->Type 1938testdata/Builtins.lc 465:51-465:62 Type->Type
1978testdata/Builtins.lc 465:51-465:64 Type 1939testdata/Builtins.lc 465:51-465:64 Type
1979testdata/Builtins.lc 465:61-465:62 V2 1940testdata/Builtins.lc 465:61-465:62 V4
1980testdata/Builtins.lc 465:63-465:64 Type 1941testdata/Builtins.lc 465:63-465:64 Type
1981testdata/Builtins.lc 465:69-465:70 Type 1942testdata/Builtins.lc 465:66-465:67 V3
1982testdata/Builtins.lc 465:69-465:83 Type 1943testdata/Builtins.lc 465:66-465:69 Type->Type
1983testdata/Builtins.lc 465:74-465:78 Type 1944testdata/Builtins.lc 465:66-465:86 Type
1984testdata/Builtins.lc 465:74-465:83 Type 1945testdata/Builtins.lc 465:66-465:102 Type
1985testdata/Builtins.lc 465:82-465:83 Type 1946testdata/Builtins.lc 465:68-465:69 Type -> Type->Type
1986testdata/Builtins.lc 467:1-467:8 Bool -> Bool->Bool 1947testdata/Builtins.lc 465:70-465:79 Nat -> Type->Type
1987testdata/Builtins.lc 467:10-467:16 Bool -> Bool->Bool 1948testdata/Builtins.lc 465:70-465:81 Type->Type
1988testdata/Builtins.lc 467:18-467:25 Bool -> Bool->Bool 1949testdata/Builtins.lc 465:70-465:86 Type
1989testdata/Builtins.lc 467:34-467:38 Type 1950testdata/Builtins.lc 465:80-465:81 Nat
1990testdata/Builtins.lc 467:42-467:46 Type 1951testdata/Builtins.lc 465:82-465:86 Type
1991testdata/Builtins.lc 467:42-467:54 Type 1952testdata/Builtins.lc 465:91-465:92 Type
1992testdata/Builtins.lc 467:50-467:54 Type 1953testdata/Builtins.lc 465:91-465:102 Type
1993testdata/Builtins.lc 468:1-468:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a 1954testdata/Builtins.lc 465:96-465:97 Type
1994testdata/Builtins.lc 468:34-468:56 Type 1955testdata/Builtins.lc 465:96-465:102 Type
1995testdata/Builtins.lc 468:34-468:66 Type 1956testdata/Builtins.lc 465:101-465:102 Type
1996testdata/Builtins.lc 468:35-468:36 V3 1957testdata/Builtins.lc 466:1-466:13 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
1997testdata/Builtins.lc 468:35-468:38 Type->Type 1958testdata/Builtins.lc 466:15-466:27 {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
1998testdata/Builtins.lc 468:37-468:38 Type -> Type->Type 1959testdata/Builtins.lc 466:34-466:83 Type
1999testdata/Builtins.lc 468:39-468:48 Nat -> Type->Type 1960testdata/Builtins.lc 466:35-466:43 Type->Type
2000testdata/Builtins.lc 468:39-468:50 Type->Type 1961testdata/Builtins.lc 466:35-466:45 Type
2001testdata/Builtins.lc 468:39-468:55 Type 1962testdata/Builtins.lc 466:44-466:45 V5
2002testdata/Builtins.lc 468:49-468:50 V1 1963testdata/Builtins.lc 466:47-466:48 V4
2003testdata/Builtins.lc 468:51-468:55 Type 1964testdata/Builtins.lc 466:47-466:50 Type->Type
2004testdata/Builtins.lc 468:60-468:61 Type 1965testdata/Builtins.lc 466:47-466:64 Type
2005testdata/Builtins.lc 468:60-468:66 Type 1966testdata/Builtins.lc 466:47-466:83 Type
2006testdata/Builtins.lc 468:65-468:66 Type 1967testdata/Builtins.lc 466:49-466:50 Type -> Type->Type
2007testdata/Builtins.lc 469:1-469:8 {a:Nat} -> VecScalar a Bool -> Bool 1968testdata/Builtins.lc 466:51-466:60 Nat -> Type->Type
2008testdata/Builtins.lc 469:10-469:17 {a:Nat} -> VecScalar a Bool -> Bool 1969testdata/Builtins.lc 466:51-466:62 Type->Type
2009testdata/Builtins.lc 469:34-469:43 Nat -> Type->Type 1970testdata/Builtins.lc 466:51-466:64 Type
2010testdata/Builtins.lc 469:34-469:45 Type->Type 1971testdata/Builtins.lc 466:61-466:62 V2
2011testdata/Builtins.lc 469:34-469:50 Type 1972testdata/Builtins.lc 466:63-466:64 Type
2012testdata/Builtins.lc 469:34-469:58 Type 1973testdata/Builtins.lc 466:69-466:70 Type
2013testdata/Builtins.lc 469:44-469:45 V1 1974testdata/Builtins.lc 466:69-466:83 Type
2014testdata/Builtins.lc 469:46-469:50 Type 1975testdata/Builtins.lc 466:74-466:78 Type
2015testdata/Builtins.lc 469:54-469:58 Type 1976testdata/Builtins.lc 466:74-466:83 Type
2016testdata/Builtins.lc 472:1-472:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1977testdata/Builtins.lc 466:82-466:83 Type
2017testdata/Builtins.lc 472:11-472:20 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1978testdata/Builtins.lc 468:1-468:8 Bool -> Bool->Bool
2018testdata/Builtins.lc 472:22-472:30 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1979testdata/Builtins.lc 468:10-468:16 Bool -> Bool->Bool
2019testdata/Builtins.lc 472:32-472:41 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1980testdata/Builtins.lc 468:18-468:25 Bool -> Bool->Bool
2020testdata/Builtins.lc 472:43-472:51 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1981testdata/Builtins.lc 468:34-468:38 Type
2021testdata/Builtins.lc 472:53-472:62 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1982testdata/Builtins.lc 468:42-468:46 Type
2022testdata/Builtins.lc 472:64-472:71 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1983testdata/Builtins.lc 468:42-468:54 Type
2023testdata/Builtins.lc 472:73-472:81 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1984testdata/Builtins.lc 468:50-468:54 Type
2024testdata/Builtins.lc 472:83-472:94 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1985testdata/Builtins.lc 469:1-469:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a
2025testdata/Builtins.lc 472:96-472:107 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1986testdata/Builtins.lc 469:34-469:56 Type
2026testdata/Builtins.lc 472:109-472:116 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1987testdata/Builtins.lc 469:34-469:66 Type
2027testdata/Builtins.lc 472:118-472:126 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1988testdata/Builtins.lc 469:35-469:36 V3
2028testdata/Builtins.lc 472:128-472:135 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1989testdata/Builtins.lc 469:35-469:38 Type->Type
2029testdata/Builtins.lc 472:137-472:145 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1990testdata/Builtins.lc 469:37-469:38 Type -> Type->Type
2030testdata/Builtins.lc 472:147-472:154 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1991testdata/Builtins.lc 469:39-469:48 Nat -> Type->Type
2031testdata/Builtins.lc 472:156-472:163 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1992testdata/Builtins.lc 469:39-469:50 Type->Type
2032testdata/Builtins.lc 472:165-472:173 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1993testdata/Builtins.lc 469:39-469:55 Type
2033testdata/Builtins.lc 472:175-472:183 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1994testdata/Builtins.lc 469:49-469:50 V1
2034testdata/Builtins.lc 472:185-472:193 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1995testdata/Builtins.lc 469:51-469:55 Type
2035testdata/Builtins.lc 472:195-472:206 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 1996testdata/Builtins.lc 469:60-469:61 Type
2036testdata/Builtins.lc 473:34-473:57 Type 1997testdata/Builtins.lc 469:60-469:66 Type
2037testdata/Builtins.lc 473:34-473:67 Type 1998testdata/Builtins.lc 469:65-469:66 Type
2038testdata/Builtins.lc 473:35-473:36 V3 1999testdata/Builtins.lc 470:1-470:8 {a:Nat} -> VecScalar a Bool -> Bool
2039testdata/Builtins.lc 473:35-473:38 Type->Type 2000testdata/Builtins.lc 470:10-470:17 {a:Nat} -> VecScalar a Bool -> Bool
2040testdata/Builtins.lc 473:37-473:38 Type -> Type->Type 2001testdata/Builtins.lc 470:34-470:43 Nat -> Type->Type
2041testdata/Builtins.lc 473:39-473:48 Nat -> Type->Type 2002testdata/Builtins.lc 470:34-470:45 Type->Type
2042testdata/Builtins.lc 473:39-473:50 Type->Type 2003testdata/Builtins.lc 470:34-470:50 Type
2043testdata/Builtins.lc 473:39-473:56 Type 2004testdata/Builtins.lc 470:34-470:58 Type
2044testdata/Builtins.lc 473:49-473:50 V1 2005testdata/Builtins.lc 470:44-470:45 V1
2045testdata/Builtins.lc 473:51-473:56 Type 2006testdata/Builtins.lc 470:46-470:50 Type
2046testdata/Builtins.lc 473:61-473:62 Type 2007testdata/Builtins.lc 470:54-470:58 Type
2047testdata/Builtins.lc 473:61-473:67 Type 2008testdata/Builtins.lc 473:1-473:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2048testdata/Builtins.lc 473:66-473:67 Type 2009testdata/Builtins.lc 473:11-473:20 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2049testdata/Builtins.lc 474:1-474:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a 2010testdata/Builtins.lc 473:22-473:30 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2050testdata/Builtins.lc 474:10-474:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a 2011testdata/Builtins.lc 473:32-473:41 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2012testdata/Builtins.lc 473:43-473:51 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2013testdata/Builtins.lc 473:53-473:62 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2014testdata/Builtins.lc 473:64-473:71 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2015testdata/Builtins.lc 473:73-473:81 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2016testdata/Builtins.lc 473:83-473:94 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2017testdata/Builtins.lc 473:96-473:107 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2018testdata/Builtins.lc 473:109-473:116 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2019testdata/Builtins.lc 473:118-473:126 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2020testdata/Builtins.lc 473:128-473:135 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2021testdata/Builtins.lc 473:137-473:145 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2022testdata/Builtins.lc 473:147-473:154 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2023testdata/Builtins.lc 473:156-473:163 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2024testdata/Builtins.lc 473:165-473:173 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2025testdata/Builtins.lc 473:175-473:183 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2026testdata/Builtins.lc 473:185-473:193 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2027testdata/Builtins.lc 473:195-473:206 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2051testdata/Builtins.lc 474:34-474:57 Type 2028testdata/Builtins.lc 474:34-474:57 Type
2052testdata/Builtins.lc 474:34-474:72 Type 2029testdata/Builtins.lc 474:34-474:67 Type
2053testdata/Builtins.lc 474:35-474:36 V3 2030testdata/Builtins.lc 474:35-474:36 V3
2054testdata/Builtins.lc 474:35-474:38 Type->Type 2031testdata/Builtins.lc 474:35-474:38 Type->Type
2055testdata/Builtins.lc 474:37-474:38 Type -> Type->Type 2032testdata/Builtins.lc 474:37-474:38 Type -> Type->Type
@@ -2059,52 +2036,46 @@ testdata/Builtins.lc 474:39-474:56 Type
2059testdata/Builtins.lc 474:49-474:50 V1 2036testdata/Builtins.lc 474:49-474:50 V1
2060testdata/Builtins.lc 474:51-474:56 Type 2037testdata/Builtins.lc 474:51-474:56 Type
2061testdata/Builtins.lc 474:61-474:62 Type 2038testdata/Builtins.lc 474:61-474:62 Type
2062testdata/Builtins.lc 474:61-474:72 Type 2039testdata/Builtins.lc 474:61-474:67 Type
2063testdata/Builtins.lc 474:66-474:67 Type 2040testdata/Builtins.lc 474:66-474:67 Type
2064testdata/Builtins.lc 474:66-474:72 Type 2041testdata/Builtins.lc 475:1-475:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
2065testdata/Builtins.lc 474:71-474:72 Type 2042testdata/Builtins.lc 475:10-475:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
2066testdata/Builtins.lc 476:1-476:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2043testdata/Builtins.lc 475:34-475:57 Type
2067testdata/Builtins.lc 476:12-476:21 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2044testdata/Builtins.lc 475:34-475:72 Type
2068testdata/Builtins.lc 476:23-476:32 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2045testdata/Builtins.lc 475:35-475:36 V3
2069testdata/Builtins.lc 476:34-476:47 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2046testdata/Builtins.lc 475:35-475:38 Type->Type
2070testdata/Builtins.lc 476:49-476:57 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2047testdata/Builtins.lc 475:37-475:38 Type -> Type->Type
2071testdata/Builtins.lc 476:59-476:68 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2048testdata/Builtins.lc 475:39-475:48 Nat -> Type->Type
2072testdata/Builtins.lc 477:34-477:57 Type 2049testdata/Builtins.lc 475:39-475:50 Type->Type
2073testdata/Builtins.lc 477:34-477:67 Type 2050testdata/Builtins.lc 475:39-475:56 Type
2074testdata/Builtins.lc 477:35-477:36 V3 2051testdata/Builtins.lc 475:49-475:50 V1
2075testdata/Builtins.lc 477:35-477:38 Type->Type 2052testdata/Builtins.lc 475:51-475:56 Type
2076testdata/Builtins.lc 477:37-477:38 Type -> Type->Type 2053testdata/Builtins.lc 475:61-475:62 Type
2077testdata/Builtins.lc 477:39-477:48 Nat -> Type->Type 2054testdata/Builtins.lc 475:61-475:72 Type
2078testdata/Builtins.lc 477:39-477:50 Type->Type 2055testdata/Builtins.lc 475:66-475:67 Type
2079testdata/Builtins.lc 477:39-477:56 Type 2056testdata/Builtins.lc 475:66-475:72 Type
2080testdata/Builtins.lc 477:49-477:50 V1 2057testdata/Builtins.lc 475:71-475:72 Type
2081testdata/Builtins.lc 477:51-477:56 Type 2058testdata/Builtins.lc 477:1-477:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2082testdata/Builtins.lc 477:61-477:62 Type 2059testdata/Builtins.lc 477:12-477:21 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2083testdata/Builtins.lc 477:61-477:67 Type 2060testdata/Builtins.lc 477:23-477:32 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2084testdata/Builtins.lc 477:66-477:67 Type 2061testdata/Builtins.lc 477:34-477:47 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2085testdata/Builtins.lc 478:1-478:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b 2062testdata/Builtins.lc 477:49-477:57 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2086testdata/Builtins.lc 478:10-478:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b 2063testdata/Builtins.lc 477:59-477:68 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2087testdata/Builtins.lc 478:34-478:75 Type 2064testdata/Builtins.lc 478:34-478:57 Type
2065testdata/Builtins.lc 478:34-478:67 Type
2066testdata/Builtins.lc 478:35-478:36 V3
2088testdata/Builtins.lc 478:35-478:38 Type->Type 2067testdata/Builtins.lc 478:35-478:38 Type->Type
2089testdata/Builtins.lc 478:35-478:40 Type 2068testdata/Builtins.lc 478:37-478:38 Type -> Type->Type
2090testdata/Builtins.lc 478:39-478:40 V5 2069testdata/Builtins.lc 478:39-478:48 Nat -> Type->Type
2091testdata/Builtins.lc 478:42-478:43 V4 2070testdata/Builtins.lc 478:39-478:50 Type->Type
2092testdata/Builtins.lc 478:42-478:45 Type->Type 2071testdata/Builtins.lc 478:39-478:56 Type
2093testdata/Builtins.lc 478:42-478:59 Type 2072testdata/Builtins.lc 478:49-478:50 V1
2094testdata/Builtins.lc 478:42-478:75 Type 2073testdata/Builtins.lc 478:51-478:56 Type
2095testdata/Builtins.lc 478:44-478:45 Type -> Type->Type 2074testdata/Builtins.lc 478:61-478:62 Type
2096testdata/Builtins.lc 478:46-478:55 Nat -> Type->Type 2075testdata/Builtins.lc 478:61-478:67 Type
2097testdata/Builtins.lc 478:46-478:57 Type->Type 2076testdata/Builtins.lc 478:66-478:67 Type
2098testdata/Builtins.lc 478:46-478:59 Type 2077testdata/Builtins.lc 479:1-479:8 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
2099testdata/Builtins.lc 478:56-478:57 V2 2078testdata/Builtins.lc 479:10-479:17 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
2100testdata/Builtins.lc 478:58-478:59 Type
2101testdata/Builtins.lc 478:64-478:65 Type
2102testdata/Builtins.lc 478:64-478:75 Type
2103testdata/Builtins.lc 478:69-478:70 Type
2104testdata/Builtins.lc 478:69-478:75 Type
2105testdata/Builtins.lc 478:74-478:75 Type
2106testdata/Builtins.lc 479:1-479:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
2107testdata/Builtins.lc 479:11-479:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
2108testdata/Builtins.lc 479:34-479:75 Type 2079testdata/Builtins.lc 479:34-479:75 Type
2109testdata/Builtins.lc 479:35-479:38 Type->Type 2080testdata/Builtins.lc 479:35-479:38 Type->Type
2110testdata/Builtins.lc 479:35-479:40 Type 2081testdata/Builtins.lc 479:35-479:40 Type
@@ -2124,89 +2095,88 @@ testdata/Builtins.lc 479:64-479:75 Type
2124testdata/Builtins.lc 479:69-479:70 Type 2095testdata/Builtins.lc 479:69-479:70 Type
2125testdata/Builtins.lc 479:69-479:75 Type 2096testdata/Builtins.lc 479:69-479:75 Type
2126testdata/Builtins.lc 479:74-479:75 Type 2097testdata/Builtins.lc 479:74-479:75 Type
2127testdata/Builtins.lc 480:1-480:10 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c 2098testdata/Builtins.lc 480:1-480:9 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
2128testdata/Builtins.lc 480:12-480:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c 2099testdata/Builtins.lc 480:11-480:19 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
2129testdata/Builtins.lc 480:34-480:89 Type 2100testdata/Builtins.lc 480:34-480:75 Type
2130testdata/Builtins.lc 480:35-480:36 V5
2131testdata/Builtins.lc 480:35-480:38 Type->Type 2101testdata/Builtins.lc 480:35-480:38 Type->Type
2132testdata/Builtins.lc 480:35-480:56 Type 2102testdata/Builtins.lc 480:35-480:40 Type
2133testdata/Builtins.lc 480:37-480:38 Type -> Type->Type 2103testdata/Builtins.lc 480:39-480:40 V5
2134testdata/Builtins.lc 480:39-480:48 Nat -> Type->Type 2104testdata/Builtins.lc 480:42-480:43 V4
2135testdata/Builtins.lc 480:39-480:50 Type->Type 2105testdata/Builtins.lc 480:42-480:45 Type->Type
2136testdata/Builtins.lc 480:39-480:56 Type 2106testdata/Builtins.lc 480:42-480:59 Type
2137testdata/Builtins.lc 480:49-480:50 V3 2107testdata/Builtins.lc 480:42-480:75 Type
2138testdata/Builtins.lc 480:51-480:56 Type 2108testdata/Builtins.lc 480:44-480:45 Type -> Type->Type
2139testdata/Builtins.lc 480:58-480:59 V2 2109testdata/Builtins.lc 480:46-480:55 Nat -> Type->Type
2140testdata/Builtins.lc 480:58-480:61 Type->Type 2110testdata/Builtins.lc 480:46-480:57 Type->Type
2141testdata/Builtins.lc 480:58-480:78 Type 2111testdata/Builtins.lc 480:46-480:59 Type
2142testdata/Builtins.lc 480:58-480:89 Type 2112testdata/Builtins.lc 480:56-480:57 V2
2143testdata/Builtins.lc 480:60-480:61 Type -> Type->Type 2113testdata/Builtins.lc 480:58-480:59 Type
2144testdata/Builtins.lc 480:62-480:71 Nat -> Type->Type 2114testdata/Builtins.lc 480:64-480:65 Type
2145testdata/Builtins.lc 480:62-480:73 Type->Type 2115testdata/Builtins.lc 480:64-480:75 Type
2146testdata/Builtins.lc 480:62-480:78 Type 2116testdata/Builtins.lc 480:69-480:70 Type
2147testdata/Builtins.lc 480:72-480:73 Nat 2117testdata/Builtins.lc 480:69-480:75 Type
2148testdata/Builtins.lc 480:74-480:78 Type 2118testdata/Builtins.lc 480:74-480:75 Type
2149testdata/Builtins.lc 480:83-480:84 Type 2119testdata/Builtins.lc 481:1-481:10 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c
2150testdata/Builtins.lc 480:83-480:89 Type 2120testdata/Builtins.lc 481:12-481:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c
2151testdata/Builtins.lc 480:88-480:89 Type 2121testdata/Builtins.lc 481:34-481:89 Type
2152testdata/Builtins.lc 481:1-481:8 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b 2122testdata/Builtins.lc 481:35-481:36 V5
2153testdata/Builtins.lc 481:10-481:18 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b 2123testdata/Builtins.lc 481:35-481:38 Type->Type
2154testdata/Builtins.lc 481:34-481:73 Type 2124testdata/Builtins.lc 481:35-481:56 Type
2155testdata/Builtins.lc 481:35-481:41 Type->Type 2125testdata/Builtins.lc 481:37-481:38 Type -> Type->Type
2156testdata/Builtins.lc 481:35-481:43 Type 2126testdata/Builtins.lc 481:39-481:48 Nat -> Type->Type
2157testdata/Builtins.lc 481:42-481:43 V5 2127testdata/Builtins.lc 481:39-481:50 Type->Type
2158testdata/Builtins.lc 481:45-481:46 V4 2128testdata/Builtins.lc 481:39-481:56 Type
2159testdata/Builtins.lc 481:45-481:48 Type->Type 2129testdata/Builtins.lc 481:49-481:50 V3
2160testdata/Builtins.lc 481:45-481:62 Type 2130testdata/Builtins.lc 481:51-481:56 Type
2161testdata/Builtins.lc 481:45-481:73 Type 2131testdata/Builtins.lc 481:58-481:59 V2
2162testdata/Builtins.lc 481:47-481:48 Type -> Type->Type 2132testdata/Builtins.lc 481:58-481:61 Type->Type
2163testdata/Builtins.lc 481:49-481:58 Nat -> Type->Type 2133testdata/Builtins.lc 481:58-481:78 Type
2164testdata/Builtins.lc 481:49-481:60 Type->Type 2134testdata/Builtins.lc 481:58-481:89 Type
2165testdata/Builtins.lc 481:49-481:62 Type 2135testdata/Builtins.lc 481:60-481:61 Type -> Type->Type
2166testdata/Builtins.lc 481:59-481:60 V2 2136testdata/Builtins.lc 481:62-481:71 Nat -> Type->Type
2167testdata/Builtins.lc 481:61-481:62 Type 2137testdata/Builtins.lc 481:62-481:73 Type->Type
2168testdata/Builtins.lc 481:67-481:68 Type 2138testdata/Builtins.lc 481:62-481:78 Type
2169testdata/Builtins.lc 481:67-481:73 Type 2139testdata/Builtins.lc 481:72-481:73 Nat
2170testdata/Builtins.lc 481:72-481:73 Type 2140testdata/Builtins.lc 481:74-481:78 Type
2171testdata/Builtins.lc 482:1-482:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> Tuple2 a a 2141testdata/Builtins.lc 481:83-481:84 Type
2172testdata/Builtins.lc 482:34-482:57 Type 2142testdata/Builtins.lc 481:83-481:89 Type
2173testdata/Builtins.lc 482:34-482:72 Type 2143testdata/Builtins.lc 481:88-481:89 Type
2174testdata/Builtins.lc 482:35-482:36 V3 2144testdata/Builtins.lc 482:1-482:8 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b
2175testdata/Builtins.lc 482:35-482:38 Type->Type 2145testdata/Builtins.lc 482:10-482:18 {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b
2176testdata/Builtins.lc 482:37-482:38 Type -> Type->Type 2146testdata/Builtins.lc 482:34-482:73 Type
2177testdata/Builtins.lc 482:39-482:48 Nat -> Type->Type 2147testdata/Builtins.lc 482:35-482:41 Type->Type
2178testdata/Builtins.lc 482:39-482:50 Type->Type 2148testdata/Builtins.lc 482:35-482:43 Type
2179testdata/Builtins.lc 482:39-482:56 Type 2149testdata/Builtins.lc 482:42-482:43 V5
2180testdata/Builtins.lc 482:49-482:50 V1 2150testdata/Builtins.lc 482:45-482:46 V4
2181testdata/Builtins.lc 482:51-482:56 Type 2151testdata/Builtins.lc 482:45-482:48 Type->Type
2152testdata/Builtins.lc 482:45-482:62 Type
2153testdata/Builtins.lc 482:45-482:73 Type
2154testdata/Builtins.lc 482:47-482:48 Type -> Type->Type
2155testdata/Builtins.lc 482:49-482:58 Nat -> Type->Type
2156testdata/Builtins.lc 482:49-482:60 Type->Type
2157testdata/Builtins.lc 482:49-482:62 Type
2158testdata/Builtins.lc 482:59-482:60 V2
2182testdata/Builtins.lc 482:61-482:62 Type 2159testdata/Builtins.lc 482:61-482:62 Type
2183testdata/Builtins.lc 482:61-482:72 Type
2184testdata/Builtins.lc 482:66-482:72 Type
2185testdata/Builtins.lc 482:67-482:68 Type 2160testdata/Builtins.lc 482:67-482:68 Type
2186testdata/Builtins.lc 482:70-482:71 Type 2161testdata/Builtins.lc 482:67-482:73 Type
2187testdata/Builtins.lc 483:1-483:10 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b -> b->b 2162testdata/Builtins.lc 482:72-482:73 Type
2188testdata/Builtins.lc 483:34-483:80 Type 2163testdata/Builtins.lc 483:1-483:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> Tuple2 a a
2164testdata/Builtins.lc 483:34-483:57 Type
2165testdata/Builtins.lc 483:34-483:72 Type
2166testdata/Builtins.lc 483:35-483:36 V3
2189testdata/Builtins.lc 483:35-483:38 Type->Type 2167testdata/Builtins.lc 483:35-483:38 Type->Type
2190testdata/Builtins.lc 483:35-483:40 Type 2168testdata/Builtins.lc 483:37-483:38 Type -> Type->Type
2191testdata/Builtins.lc 483:39-483:40 V5 2169testdata/Builtins.lc 483:39-483:48 Nat -> Type->Type
2192testdata/Builtins.lc 483:42-483:43 V4 2170testdata/Builtins.lc 483:39-483:50 Type->Type
2193testdata/Builtins.lc 483:42-483:45 Type->Type 2171testdata/Builtins.lc 483:39-483:56 Type
2194testdata/Builtins.lc 483:42-483:59 Type 2172testdata/Builtins.lc 483:49-483:50 V1
2195testdata/Builtins.lc 483:42-483:80 Type 2173testdata/Builtins.lc 483:51-483:56 Type
2196testdata/Builtins.lc 483:44-483:45 Type -> Type->Type 2174testdata/Builtins.lc 483:61-483:62 Type
2197testdata/Builtins.lc 483:46-483:55 Nat -> Type->Type 2175testdata/Builtins.lc 483:61-483:72 Type
2198testdata/Builtins.lc 483:46-483:57 Type->Type 2176testdata/Builtins.lc 483:66-483:72 Type
2199testdata/Builtins.lc 483:46-483:59 Type 2177testdata/Builtins.lc 483:67-483:68 Type
2200testdata/Builtins.lc 483:56-483:57 V2 2178testdata/Builtins.lc 483:70-483:71 Type
2201testdata/Builtins.lc 483:58-483:59 Type 2179testdata/Builtins.lc 484:1-484:10 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b -> b->b
2202testdata/Builtins.lc 483:64-483:65 Type
2203testdata/Builtins.lc 483:64-483:80 Type
2204testdata/Builtins.lc 483:69-483:70 Type
2205testdata/Builtins.lc 483:69-483:80 Type
2206testdata/Builtins.lc 483:74-483:75 Type
2207testdata/Builtins.lc 483:74-483:80 Type
2208testdata/Builtins.lc 483:79-483:80 Type
2209testdata/Builtins.lc 484:1-484:11 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a -> a->b
2210testdata/Builtins.lc 484:34-484:80 Type 2180testdata/Builtins.lc 484:34-484:80 Type
2211testdata/Builtins.lc 484:35-484:38 Type->Type 2181testdata/Builtins.lc 484:35-484:38 Type->Type
2212testdata/Builtins.lc 484:35-484:40 Type 2182testdata/Builtins.lc 484:35-484:40 Type
@@ -2228,27 +2198,31 @@ testdata/Builtins.lc 484:69-484:80 Type
2228testdata/Builtins.lc 484:74-484:75 Type 2198testdata/Builtins.lc 484:74-484:75 Type
2229testdata/Builtins.lc 484:74-484:80 Type 2199testdata/Builtins.lc 484:74-484:80 Type
2230testdata/Builtins.lc 484:79-484:80 Type 2200testdata/Builtins.lc 484:79-484:80 Type
2231testdata/Builtins.lc 485:1-485:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a 2201testdata/Builtins.lc 485:1-485:11 {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a -> a->b
2232testdata/Builtins.lc 485:34-485:57 Type 2202testdata/Builtins.lc 485:34-485:80 Type
2233testdata/Builtins.lc 485:34-485:77 Type
2234testdata/Builtins.lc 485:35-485:36 V3
2235testdata/Builtins.lc 485:35-485:38 Type->Type 2203testdata/Builtins.lc 485:35-485:38 Type->Type
2236testdata/Builtins.lc 485:37-485:38 Type -> Type->Type 2204testdata/Builtins.lc 485:35-485:40 Type
2237testdata/Builtins.lc 485:39-485:48 Nat -> Type->Type 2205testdata/Builtins.lc 485:39-485:40 V5
2238testdata/Builtins.lc 485:39-485:50 Type->Type 2206testdata/Builtins.lc 485:42-485:43 V4
2239testdata/Builtins.lc 485:39-485:56 Type 2207testdata/Builtins.lc 485:42-485:45 Type->Type
2240testdata/Builtins.lc 485:49-485:50 V1 2208testdata/Builtins.lc 485:42-485:59 Type
2241testdata/Builtins.lc 485:51-485:56 Type 2209testdata/Builtins.lc 485:42-485:80 Type
2242testdata/Builtins.lc 485:61-485:62 Type 2210testdata/Builtins.lc 485:44-485:45 Type -> Type->Type
2243testdata/Builtins.lc 485:61-485:77 Type 2211testdata/Builtins.lc 485:46-485:55 Nat -> Type->Type
2244testdata/Builtins.lc 485:66-485:67 Type 2212testdata/Builtins.lc 485:46-485:57 Type->Type
2245testdata/Builtins.lc 485:66-485:77 Type 2213testdata/Builtins.lc 485:46-485:59 Type
2246testdata/Builtins.lc 485:71-485:72 Type 2214testdata/Builtins.lc 485:56-485:57 V2
2247testdata/Builtins.lc 485:71-485:77 Type 2215testdata/Builtins.lc 485:58-485:59 Type
2248testdata/Builtins.lc 485:76-485:77 Type 2216testdata/Builtins.lc 485:64-485:65 Type
2249testdata/Builtins.lc 486:1-486:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> Float->a 2217testdata/Builtins.lc 485:64-485:80 Type
2218testdata/Builtins.lc 485:69-485:70 Type
2219testdata/Builtins.lc 485:69-485:80 Type
2220testdata/Builtins.lc 485:74-485:75 Type
2221testdata/Builtins.lc 485:74-485:80 Type
2222testdata/Builtins.lc 485:79-485:80 Type
2223testdata/Builtins.lc 486:1-486:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
2250testdata/Builtins.lc 486:34-486:57 Type 2224testdata/Builtins.lc 486:34-486:57 Type
2251testdata/Builtins.lc 486:34-486:81 Type 2225testdata/Builtins.lc 486:34-486:77 Type
2252testdata/Builtins.lc 486:35-486:36 V3 2226testdata/Builtins.lc 486:35-486:36 V3
2253testdata/Builtins.lc 486:35-486:38 Type->Type 2227testdata/Builtins.lc 486:35-486:38 Type->Type
2254testdata/Builtins.lc 486:37-486:38 Type -> Type->Type 2228testdata/Builtins.lc 486:37-486:38 Type -> Type->Type
@@ -2258,174 +2232,177 @@ testdata/Builtins.lc 486:39-486:56 Type
2258testdata/Builtins.lc 486:49-486:50 V1 2232testdata/Builtins.lc 486:49-486:50 V1
2259testdata/Builtins.lc 486:51-486:56 Type 2233testdata/Builtins.lc 486:51-486:56 Type
2260testdata/Builtins.lc 486:61-486:62 Type 2234testdata/Builtins.lc 486:61-486:62 Type
2261testdata/Builtins.lc 486:61-486:81 Type 2235testdata/Builtins.lc 486:61-486:77 Type
2262testdata/Builtins.lc 486:66-486:67 Type 2236testdata/Builtins.lc 486:66-486:67 Type
2263testdata/Builtins.lc 486:66-486:81 Type 2237testdata/Builtins.lc 486:66-486:77 Type
2264testdata/Builtins.lc 486:71-486:76 Type 2238testdata/Builtins.lc 486:71-486:72 Type
2265testdata/Builtins.lc 486:71-486:81 Type 2239testdata/Builtins.lc 486:71-486:77 Type
2266testdata/Builtins.lc 486:80-486:81 Type 2240testdata/Builtins.lc 486:76-486:77 Type
2267testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a 2241testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> Float->a
2268testdata/Builtins.lc 487:34-487:99 Type 2242testdata/Builtins.lc 487:34-487:57 Type
2269testdata/Builtins.lc 487:35-487:36 V5 2243testdata/Builtins.lc 487:34-487:81 Type
2244testdata/Builtins.lc 487:35-487:36 V3
2270testdata/Builtins.lc 487:35-487:38 Type->Type 2245testdata/Builtins.lc 487:35-487:38 Type->Type
2271testdata/Builtins.lc 487:35-487:56 Type
2272testdata/Builtins.lc 487:37-487:38 Type -> Type->Type 2246testdata/Builtins.lc 487:37-487:38 Type -> Type->Type
2273testdata/Builtins.lc 487:39-487:48 Nat -> Type->Type 2247testdata/Builtins.lc 487:39-487:48 Nat -> Type->Type
2274testdata/Builtins.lc 487:39-487:50 Type->Type 2248testdata/Builtins.lc 487:39-487:50 Type->Type
2275testdata/Builtins.lc 487:39-487:56 Type 2249testdata/Builtins.lc 487:39-487:56 Type
2276testdata/Builtins.lc 487:49-487:50 V3 2250testdata/Builtins.lc 487:49-487:50 V1
2277testdata/Builtins.lc 487:51-487:56 Type 2251testdata/Builtins.lc 487:51-487:56 Type
2278testdata/Builtins.lc 487:58-487:59 V2 2252testdata/Builtins.lc 487:61-487:62 Type
2279testdata/Builtins.lc 487:58-487:61 Type->Type 2253testdata/Builtins.lc 487:61-487:81 Type
2280testdata/Builtins.lc 487:58-487:78 Type 2254testdata/Builtins.lc 487:66-487:67 Type
2281testdata/Builtins.lc 487:58-487:99 Type 2255testdata/Builtins.lc 487:66-487:81 Type
2282testdata/Builtins.lc 487:60-487:61 Type -> Type->Type 2256testdata/Builtins.lc 487:71-487:76 Type
2283testdata/Builtins.lc 487:62-487:71 Nat -> Type->Type 2257testdata/Builtins.lc 487:71-487:81 Type
2284testdata/Builtins.lc 487:62-487:73 Type->Type 2258testdata/Builtins.lc 487:80-487:81 Type
2285testdata/Builtins.lc 487:62-487:78 Type 2259testdata/Builtins.lc 488:1-488:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a
2286testdata/Builtins.lc 487:72-487:73 Nat 2260testdata/Builtins.lc 488:34-488:99 Type
2287testdata/Builtins.lc 487:74-487:78 Type 2261testdata/Builtins.lc 488:35-488:36 V5
2288testdata/Builtins.lc 487:83-487:84 Type
2289testdata/Builtins.lc 487:83-487:99 Type
2290testdata/Builtins.lc 487:88-487:89 Type
2291testdata/Builtins.lc 487:88-487:99 Type
2292testdata/Builtins.lc 487:93-487:94 Type
2293testdata/Builtins.lc 487:93-487:99 Type
2294testdata/Builtins.lc 487:98-487:99 Type
2295testdata/Builtins.lc 488:1-488:9 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a->a
2296testdata/Builtins.lc 488:34-488:53 Type
2297testdata/Builtins.lc 488:34-488:68 Type
2298testdata/Builtins.lc 488:35-488:36 V3
2299testdata/Builtins.lc 488:35-488:38 Type->Type 2262testdata/Builtins.lc 488:35-488:38 Type->Type
2263testdata/Builtins.lc 488:35-488:56 Type
2300testdata/Builtins.lc 488:37-488:38 Type -> Type->Type 2264testdata/Builtins.lc 488:37-488:38 Type -> Type->Type
2301testdata/Builtins.lc 488:39-488:44 Nat -> Type->Type 2265testdata/Builtins.lc 488:39-488:48 Nat -> Type->Type
2302testdata/Builtins.lc 488:39-488:46 Type->Type 2266testdata/Builtins.lc 488:39-488:50 Type->Type
2303testdata/Builtins.lc 488:39-488:52 Type 2267testdata/Builtins.lc 488:39-488:56 Type
2304testdata/Builtins.lc 488:45-488:46 V1 2268testdata/Builtins.lc 488:49-488:50 V3
2305testdata/Builtins.lc 488:47-488:52 Type 2269testdata/Builtins.lc 488:51-488:56 Type
2306testdata/Builtins.lc 488:57-488:58 Type 2270testdata/Builtins.lc 488:58-488:59 V2
2307testdata/Builtins.lc 488:57-488:68 Type 2271testdata/Builtins.lc 488:58-488:61 Type->Type
2308testdata/Builtins.lc 488:62-488:63 Type 2272testdata/Builtins.lc 488:58-488:78 Type
2309testdata/Builtins.lc 488:62-488:68 Type 2273testdata/Builtins.lc 488:58-488:99 Type
2310testdata/Builtins.lc 488:67-488:68 Type 2274testdata/Builtins.lc 488:60-488:61 Type -> Type->Type
2311testdata/Builtins.lc 489:1-489:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> a->a 2275testdata/Builtins.lc 488:62-488:71 Nat -> Type->Type
2312testdata/Builtins.lc 489:34-489:57 Type 2276testdata/Builtins.lc 488:62-488:73 Type->Type
2313testdata/Builtins.lc 489:34-489:76 Type 2277testdata/Builtins.lc 488:62-488:78 Type
2278testdata/Builtins.lc 488:72-488:73 Nat
2279testdata/Builtins.lc 488:74-488:78 Type
2280testdata/Builtins.lc 488:83-488:84 Type
2281testdata/Builtins.lc 488:83-488:99 Type
2282testdata/Builtins.lc 488:88-488:89 Type
2283testdata/Builtins.lc 488:88-488:99 Type
2284testdata/Builtins.lc 488:93-488:94 Type
2285testdata/Builtins.lc 488:93-488:99 Type
2286testdata/Builtins.lc 488:98-488:99 Type
2287testdata/Builtins.lc 489:1-489:9 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a->a
2288testdata/Builtins.lc 489:34-489:53 Type
2289testdata/Builtins.lc 489:34-489:68 Type
2314testdata/Builtins.lc 489:35-489:36 V3 2290testdata/Builtins.lc 489:35-489:36 V3
2315testdata/Builtins.lc 489:35-489:38 Type->Type 2291testdata/Builtins.lc 489:35-489:38 Type->Type
2316testdata/Builtins.lc 489:37-489:38 Type -> Type->Type 2292testdata/Builtins.lc 489:37-489:38 Type -> Type->Type
2317testdata/Builtins.lc 489:39-489:48 Nat -> Type->Type 2293testdata/Builtins.lc 489:39-489:44 Nat -> Type->Type
2318testdata/Builtins.lc 489:39-489:50 Type->Type 2294testdata/Builtins.lc 489:39-489:46 Type->Type
2319testdata/Builtins.lc 489:39-489:56 Type 2295testdata/Builtins.lc 489:39-489:52 Type
2320testdata/Builtins.lc 489:49-489:50 V1 2296testdata/Builtins.lc 489:45-489:46 V1
2321testdata/Builtins.lc 489:51-489:56 Type 2297testdata/Builtins.lc 489:47-489:52 Type
2322testdata/Builtins.lc 489:61-489:66 Type 2298testdata/Builtins.lc 489:57-489:58 Type
2323testdata/Builtins.lc 489:61-489:76 Type 2299testdata/Builtins.lc 489:57-489:68 Type
2324testdata/Builtins.lc 489:70-489:71 Type 2300testdata/Builtins.lc 489:62-489:63 Type
2325testdata/Builtins.lc 489:70-489:76 Type 2301testdata/Builtins.lc 489:62-489:68 Type
2326testdata/Builtins.lc 489:75-489:76 Type 2302testdata/Builtins.lc 489:67-489:68 Type
2327testdata/Builtins.lc 490:1-490:15 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a -> a->a 2303testdata/Builtins.lc 490:1-490:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> a->a
2328testdata/Builtins.lc 490:34-490:53 Type 2304testdata/Builtins.lc 490:34-490:57 Type
2329testdata/Builtins.lc 490:34-490:73 Type 2305testdata/Builtins.lc 490:34-490:76 Type
2330testdata/Builtins.lc 490:35-490:36 V3 2306testdata/Builtins.lc 490:35-490:36 V3
2331testdata/Builtins.lc 490:35-490:38 Type->Type 2307testdata/Builtins.lc 490:35-490:38 Type->Type
2332testdata/Builtins.lc 490:37-490:38 Type -> Type->Type 2308testdata/Builtins.lc 490:37-490:38 Type -> Type->Type
2333testdata/Builtins.lc 490:39-490:44 Nat -> Type->Type 2309testdata/Builtins.lc 490:39-490:48 Nat -> Type->Type
2334testdata/Builtins.lc 490:39-490:46 Type->Type 2310testdata/Builtins.lc 490:39-490:50 Type->Type
2335testdata/Builtins.lc 490:39-490:52 Type 2311testdata/Builtins.lc 490:39-490:56 Type
2336testdata/Builtins.lc 490:45-490:46 V1 2312testdata/Builtins.lc 490:49-490:50 V1
2337testdata/Builtins.lc 490:47-490:52 Type 2313testdata/Builtins.lc 490:51-490:56 Type
2338testdata/Builtins.lc 490:57-490:58 Type 2314testdata/Builtins.lc 490:61-490:66 Type
2339testdata/Builtins.lc 490:57-490:73 Type 2315testdata/Builtins.lc 490:61-490:76 Type
2340testdata/Builtins.lc 490:62-490:63 Type 2316testdata/Builtins.lc 490:70-490:71 Type
2341testdata/Builtins.lc 490:62-490:73 Type 2317testdata/Builtins.lc 490:70-490:76 Type
2342testdata/Builtins.lc 490:67-490:68 Type 2318testdata/Builtins.lc 490:75-490:76 Type
2343testdata/Builtins.lc 490:67-490:73 Type 2319testdata/Builtins.lc 491:1-491:15 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a -> a->a
2344testdata/Builtins.lc 490:72-490:73 Type 2320testdata/Builtins.lc 491:34-491:53 Type
2345testdata/Builtins.lc 491:1-491:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> Float -> a->a 2321testdata/Builtins.lc 491:34-491:73 Type
2346testdata/Builtins.lc 491:34-491:57 Type
2347testdata/Builtins.lc 491:34-491:85 Type
2348testdata/Builtins.lc 491:35-491:36 V3 2322testdata/Builtins.lc 491:35-491:36 V3
2349testdata/Builtins.lc 491:35-491:38 Type->Type 2323testdata/Builtins.lc 491:35-491:38 Type->Type
2350testdata/Builtins.lc 491:37-491:38 Type -> Type->Type 2324testdata/Builtins.lc 491:37-491:38 Type -> Type->Type
2351testdata/Builtins.lc 491:39-491:48 Nat -> Type->Type 2325testdata/Builtins.lc 491:39-491:44 Nat -> Type->Type
2352testdata/Builtins.lc 491:39-491:50 Type->Type 2326testdata/Builtins.lc 491:39-491:46 Type->Type
2353testdata/Builtins.lc 491:39-491:56 Type 2327testdata/Builtins.lc 491:39-491:52 Type
2354testdata/Builtins.lc 491:49-491:50 V1 2328testdata/Builtins.lc 491:45-491:46 V1
2355testdata/Builtins.lc 491:51-491:56 Type 2329testdata/Builtins.lc 491:47-491:52 Type
2356testdata/Builtins.lc 491:61-491:66 Type 2330testdata/Builtins.lc 491:57-491:58 Type
2357testdata/Builtins.lc 491:61-491:85 Type 2331testdata/Builtins.lc 491:57-491:73 Type
2358testdata/Builtins.lc 491:70-491:75 Type 2332testdata/Builtins.lc 491:62-491:63 Type
2359testdata/Builtins.lc 491:70-491:85 Type 2333testdata/Builtins.lc 491:62-491:73 Type
2360testdata/Builtins.lc 491:79-491:80 Type 2334testdata/Builtins.lc 491:67-491:68 Type
2361testdata/Builtins.lc 491:79-491:85 Type 2335testdata/Builtins.lc 491:67-491:73 Type
2362testdata/Builtins.lc 491:84-491:85 Type 2336testdata/Builtins.lc 491:72-491:73 Type
2363testdata/Builtins.lc 494:1-494:19 {a:Nat} -> VecScalar a Float -> VecScalar a Int 2337testdata/Builtins.lc 492:1-492:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> Float -> a->a
2364testdata/Builtins.lc 494:34-494:43 Nat -> Type->Type 2338testdata/Builtins.lc 492:34-492:57 Type
2365testdata/Builtins.lc 494:34-494:45 Type->Type 2339testdata/Builtins.lc 492:34-492:85 Type
2366testdata/Builtins.lc 494:34-494:51 Type 2340testdata/Builtins.lc 492:35-492:36 V3
2367testdata/Builtins.lc 494:34-494:70 Type 2341testdata/Builtins.lc 492:35-492:38 Type->Type
2368testdata/Builtins.lc 494:44-494:45 V1 2342testdata/Builtins.lc 492:37-492:38 Type -> Type->Type
2369testdata/Builtins.lc 494:46-494:51 Type 2343testdata/Builtins.lc 492:39-492:48 Nat -> Type->Type
2370testdata/Builtins.lc 494:55-494:64 Nat -> Type->Type 2344testdata/Builtins.lc 492:39-492:50 Type->Type
2371testdata/Builtins.lc 494:55-494:66 Type->Type 2345testdata/Builtins.lc 492:39-492:56 Type
2372testdata/Builtins.lc 494:55-494:70 Type 2346testdata/Builtins.lc 492:49-492:50 V1
2373testdata/Builtins.lc 494:65-494:66 Nat 2347testdata/Builtins.lc 492:51-492:56 Type
2374testdata/Builtins.lc 494:67-494:70 Type 2348testdata/Builtins.lc 492:61-492:66 Type
2375testdata/Builtins.lc 495:1-495:20 {a:Nat} -> VecScalar a Float -> VecScalar a Word 2349testdata/Builtins.lc 492:61-492:85 Type
2350testdata/Builtins.lc 492:70-492:75 Type
2351testdata/Builtins.lc 492:70-492:85 Type
2352testdata/Builtins.lc 492:79-492:80 Type
2353testdata/Builtins.lc 492:79-492:85 Type
2354testdata/Builtins.lc 492:84-492:85 Type
2355testdata/Builtins.lc 495:1-495:19 {a:Nat} -> VecScalar a Float -> VecScalar a Int
2376testdata/Builtins.lc 495:34-495:43 Nat -> Type->Type 2356testdata/Builtins.lc 495:34-495:43 Nat -> Type->Type
2377testdata/Builtins.lc 495:34-495:45 Type->Type 2357testdata/Builtins.lc 495:34-495:45 Type->Type
2378testdata/Builtins.lc 495:34-495:51 Type 2358testdata/Builtins.lc 495:34-495:51 Type
2379testdata/Builtins.lc 495:34-495:71 Type 2359testdata/Builtins.lc 495:34-495:70 Type
2380testdata/Builtins.lc 495:44-495:45 V1 2360testdata/Builtins.lc 495:44-495:45 V1
2381testdata/Builtins.lc 495:46-495:51 Type 2361testdata/Builtins.lc 495:46-495:51 Type
2382testdata/Builtins.lc 495:55-495:64 Nat -> Type->Type 2362testdata/Builtins.lc 495:55-495:64 Nat -> Type->Type
2383testdata/Builtins.lc 495:55-495:66 Type->Type 2363testdata/Builtins.lc 495:55-495:66 Type->Type
2384testdata/Builtins.lc 495:55-495:71 Type 2364testdata/Builtins.lc 495:55-495:70 Type
2385testdata/Builtins.lc 495:65-495:66 Nat 2365testdata/Builtins.lc 495:65-495:66 Nat
2386testdata/Builtins.lc 495:67-495:71 Type 2366testdata/Builtins.lc 495:67-495:70 Type
2387testdata/Builtins.lc 496:1-496:19 {a:Nat} -> VecScalar a Int -> VecScalar a Float 2367testdata/Builtins.lc 496:1-496:20 {a:Nat} -> VecScalar a Float -> VecScalar a Word
2388testdata/Builtins.lc 496:34-496:43 Nat -> Type->Type 2368testdata/Builtins.lc 496:34-496:43 Nat -> Type->Type
2389testdata/Builtins.lc 496:34-496:45 Type->Type 2369testdata/Builtins.lc 496:34-496:45 Type->Type
2390testdata/Builtins.lc 496:34-496:49 Type 2370testdata/Builtins.lc 496:34-496:51 Type
2391testdata/Builtins.lc 496:34-496:72 Type 2371testdata/Builtins.lc 496:34-496:71 Type
2392testdata/Builtins.lc 496:44-496:45 V1 2372testdata/Builtins.lc 496:44-496:45 V1
2393testdata/Builtins.lc 496:46-496:49 Type 2373testdata/Builtins.lc 496:46-496:51 Type
2394testdata/Builtins.lc 496:55-496:64 Nat -> Type->Type 2374testdata/Builtins.lc 496:55-496:64 Nat -> Type->Type
2395testdata/Builtins.lc 496:55-496:66 Type->Type 2375testdata/Builtins.lc 496:55-496:66 Type->Type
2396testdata/Builtins.lc 496:55-496:72 Type 2376testdata/Builtins.lc 496:55-496:71 Type
2397testdata/Builtins.lc 496:65-496:66 Nat 2377testdata/Builtins.lc 496:65-496:66 Nat
2398testdata/Builtins.lc 496:67-496:72 Type 2378testdata/Builtins.lc 496:67-496:71 Type
2399testdata/Builtins.lc 497:1-497:20 {a:Nat} -> VecScalar a Word -> VecScalar a Float 2379testdata/Builtins.lc 497:1-497:19 {a:Nat} -> VecScalar a Int -> VecScalar a Float
2400testdata/Builtins.lc 497:34-497:43 Nat -> Type->Type 2380testdata/Builtins.lc 497:34-497:43 Nat -> Type->Type
2401testdata/Builtins.lc 497:34-497:45 Type->Type 2381testdata/Builtins.lc 497:34-497:45 Type->Type
2402testdata/Builtins.lc 497:34-497:50 Type 2382testdata/Builtins.lc 497:34-497:49 Type
2403testdata/Builtins.lc 497:34-497:72 Type 2383testdata/Builtins.lc 497:34-497:72 Type
2404testdata/Builtins.lc 497:44-497:45 V1 2384testdata/Builtins.lc 497:44-497:45 V1
2405testdata/Builtins.lc 497:46-497:50 Type 2385testdata/Builtins.lc 497:46-497:49 Type
2406testdata/Builtins.lc 497:55-497:64 Nat -> Type->Type 2386testdata/Builtins.lc 497:55-497:64 Nat -> Type->Type
2407testdata/Builtins.lc 497:55-497:66 Type->Type 2387testdata/Builtins.lc 497:55-497:66 Type->Type
2408testdata/Builtins.lc 497:55-497:72 Type 2388testdata/Builtins.lc 497:55-497:72 Type
2409testdata/Builtins.lc 497:65-497:66 Nat 2389testdata/Builtins.lc 497:65-497:66 Nat
2410testdata/Builtins.lc 497:67-497:72 Type 2390testdata/Builtins.lc 497:67-497:72 Type
2411testdata/Builtins.lc 499:1-499:11 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->Float 2391testdata/Builtins.lc 498:1-498:20 {a:Nat} -> VecScalar a Word -> VecScalar a Float
2412testdata/Builtins.lc 499:34-499:57 Type 2392testdata/Builtins.lc 498:34-498:43 Nat -> Type->Type
2413testdata/Builtins.lc 499:34-499:71 Type 2393testdata/Builtins.lc 498:34-498:45 Type->Type
2414testdata/Builtins.lc 499:35-499:36 V3 2394testdata/Builtins.lc 498:34-498:50 Type
2415testdata/Builtins.lc 499:35-499:38 Type->Type 2395testdata/Builtins.lc 498:34-498:72 Type
2416testdata/Builtins.lc 499:37-499:38 Type -> Type->Type 2396testdata/Builtins.lc 498:44-498:45 V1
2417testdata/Builtins.lc 499:39-499:48 Nat -> Type->Type 2397testdata/Builtins.lc 498:46-498:50 Type
2418testdata/Builtins.lc 499:39-499:50 Type->Type 2398testdata/Builtins.lc 498:55-498:64 Nat -> Type->Type
2419testdata/Builtins.lc 499:39-499:56 Type 2399testdata/Builtins.lc 498:55-498:66 Type->Type
2420testdata/Builtins.lc 499:49-499:50 V1 2400testdata/Builtins.lc 498:55-498:72 Type
2421testdata/Builtins.lc 499:51-499:56 Type 2401testdata/Builtins.lc 498:65-498:66 Nat
2422testdata/Builtins.lc 499:61-499:62 Type 2402testdata/Builtins.lc 498:67-498:72 Type
2423testdata/Builtins.lc 499:61-499:71 Type 2403testdata/Builtins.lc 500:1-500:11 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->Float
2424testdata/Builtins.lc 499:66-499:71 Type
2425testdata/Builtins.lc 500:1-500:13 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
2426testdata/Builtins.lc 500:15-500:22 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
2427testdata/Builtins.lc 500:34-500:57 Type 2404testdata/Builtins.lc 500:34-500:57 Type
2428testdata/Builtins.lc 500:34-500:76 Type 2405testdata/Builtins.lc 500:34-500:71 Type
2429testdata/Builtins.lc 500:35-500:36 V3 2406testdata/Builtins.lc 500:35-500:36 V3
2430testdata/Builtins.lc 500:35-500:38 Type->Type 2407testdata/Builtins.lc 500:35-500:38 Type->Type
2431testdata/Builtins.lc 500:37-500:38 Type -> Type->Type 2408testdata/Builtins.lc 500:37-500:38 Type -> Type->Type
@@ -2435,14 +2412,13 @@ testdata/Builtins.lc 500:39-500:56 Type
2435testdata/Builtins.lc 500:49-500:50 V1 2412testdata/Builtins.lc 500:49-500:50 V1
2436testdata/Builtins.lc 500:51-500:56 Type 2413testdata/Builtins.lc 500:51-500:56 Type
2437testdata/Builtins.lc 500:61-500:62 Type 2414testdata/Builtins.lc 500:61-500:62 Type
2438testdata/Builtins.lc 500:61-500:76 Type 2415testdata/Builtins.lc 500:61-500:71 Type
2439testdata/Builtins.lc 500:66-500:67 Type 2416testdata/Builtins.lc 500:66-500:71 Type
2440testdata/Builtins.lc 500:66-500:76 Type 2417testdata/Builtins.lc 501:1-501:13 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
2441testdata/Builtins.lc 500:71-500:76 Type 2418testdata/Builtins.lc 501:15-501:22 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
2442testdata/Builtins.lc 501:1-501:10 {a} -> {b : a ~ VecS Float 3} -> a -> a->a
2443testdata/Builtins.lc 501:34-501:57 Type 2419testdata/Builtins.lc 501:34-501:57 Type
2444testdata/Builtins.lc 501:34-501:72 Type 2420testdata/Builtins.lc 501:34-501:76 Type
2445testdata/Builtins.lc 501:35-501:36 V1 2421testdata/Builtins.lc 501:35-501:36 V3
2446testdata/Builtins.lc 501:35-501:38 Type->Type 2422testdata/Builtins.lc 501:35-501:38 Type->Type
2447testdata/Builtins.lc 501:37-501:38 Type -> Type->Type 2423testdata/Builtins.lc 501:37-501:38 Type -> Type->Type
2448testdata/Builtins.lc 501:39-501:48 Nat -> Type->Type 2424testdata/Builtins.lc 501:39-501:48 Nat -> Type->Type
@@ -2451,14 +2427,14 @@ testdata/Builtins.lc 501:39-501:56 Type
2451testdata/Builtins.lc 501:49-501:50 V1 2427testdata/Builtins.lc 501:49-501:50 V1
2452testdata/Builtins.lc 501:51-501:56 Type 2428testdata/Builtins.lc 501:51-501:56 Type
2453testdata/Builtins.lc 501:61-501:62 Type 2429testdata/Builtins.lc 501:61-501:62 Type
2454testdata/Builtins.lc 501:61-501:72 Type 2430testdata/Builtins.lc 501:61-501:76 Type
2455testdata/Builtins.lc 501:66-501:67 Type 2431testdata/Builtins.lc 501:66-501:67 Type
2456testdata/Builtins.lc 501:66-501:72 Type 2432testdata/Builtins.lc 501:66-501:76 Type
2457testdata/Builtins.lc 501:71-501:72 Type 2433testdata/Builtins.lc 501:71-501:76 Type
2458testdata/Builtins.lc 502:1-502:14 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2434testdata/Builtins.lc 502:1-502:10 {a} -> {b : a ~ VecS Float 3} -> a -> a->a
2459testdata/Builtins.lc 502:34-502:57 Type 2435testdata/Builtins.lc 502:34-502:57 Type
2460testdata/Builtins.lc 502:34-502:67 Type 2436testdata/Builtins.lc 502:34-502:72 Type
2461testdata/Builtins.lc 502:35-502:36 V3 2437testdata/Builtins.lc 502:35-502:36 V1
2462testdata/Builtins.lc 502:35-502:38 Type->Type 2438testdata/Builtins.lc 502:35-502:38 Type->Type
2463testdata/Builtins.lc 502:37-502:38 Type -> Type->Type 2439testdata/Builtins.lc 502:37-502:38 Type -> Type->Type
2464testdata/Builtins.lc 502:39-502:48 Nat -> Type->Type 2440testdata/Builtins.lc 502:39-502:48 Nat -> Type->Type
@@ -2467,12 +2443,13 @@ testdata/Builtins.lc 502:39-502:56 Type
2467testdata/Builtins.lc 502:49-502:50 V1 2443testdata/Builtins.lc 502:49-502:50 V1
2468testdata/Builtins.lc 502:51-502:56 Type 2444testdata/Builtins.lc 502:51-502:56 Type
2469testdata/Builtins.lc 502:61-502:62 Type 2445testdata/Builtins.lc 502:61-502:62 Type
2470testdata/Builtins.lc 502:61-502:67 Type 2446testdata/Builtins.lc 502:61-502:72 Type
2471testdata/Builtins.lc 502:66-502:67 Type 2447testdata/Builtins.lc 502:66-502:67 Type
2472testdata/Builtins.lc 503:1-503:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a 2448testdata/Builtins.lc 502:66-502:72 Type
2473testdata/Builtins.lc 503:18-503:29 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a 2449testdata/Builtins.lc 502:71-502:72 Type
2450testdata/Builtins.lc 503:1-503:14 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2474testdata/Builtins.lc 503:34-503:57 Type 2451testdata/Builtins.lc 503:34-503:57 Type
2475testdata/Builtins.lc 503:34-503:77 Type 2452testdata/Builtins.lc 503:34-503:67 Type
2476testdata/Builtins.lc 503:35-503:36 V3 2453testdata/Builtins.lc 503:35-503:36 V3
2477testdata/Builtins.lc 503:35-503:38 Type->Type 2454testdata/Builtins.lc 503:35-503:38 Type->Type
2478testdata/Builtins.lc 503:37-503:38 Type -> Type->Type 2455testdata/Builtins.lc 503:37-503:38 Type -> Type->Type
@@ -2482,15 +2459,12 @@ testdata/Builtins.lc 503:39-503:56 Type
2482testdata/Builtins.lc 503:49-503:50 V1 2459testdata/Builtins.lc 503:49-503:50 V1
2483testdata/Builtins.lc 503:51-503:56 Type 2460testdata/Builtins.lc 503:51-503:56 Type
2484testdata/Builtins.lc 503:61-503:62 Type 2461testdata/Builtins.lc 503:61-503:62 Type
2485testdata/Builtins.lc 503:61-503:77 Type 2462testdata/Builtins.lc 503:61-503:67 Type
2486testdata/Builtins.lc 503:66-503:67 Type 2463testdata/Builtins.lc 503:66-503:67 Type
2487testdata/Builtins.lc 503:66-503:77 Type 2464testdata/Builtins.lc 504:1-504:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
2488testdata/Builtins.lc 503:71-503:72 Type 2465testdata/Builtins.lc 504:18-504:29 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
2489testdata/Builtins.lc 503:71-503:77 Type
2490testdata/Builtins.lc 503:76-503:77 Type
2491testdata/Builtins.lc 504:1-504:12 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
2492testdata/Builtins.lc 504:34-504:57 Type 2466testdata/Builtins.lc 504:34-504:57 Type
2493testdata/Builtins.lc 504:34-504:72 Type 2467testdata/Builtins.lc 504:34-504:77 Type
2494testdata/Builtins.lc 504:35-504:36 V3 2468testdata/Builtins.lc 504:35-504:36 V3
2495testdata/Builtins.lc 504:35-504:38 Type->Type 2469testdata/Builtins.lc 504:35-504:38 Type->Type
2496testdata/Builtins.lc 504:37-504:38 Type -> Type->Type 2470testdata/Builtins.lc 504:37-504:38 Type -> Type->Type
@@ -2500,223 +2474,229 @@ testdata/Builtins.lc 504:39-504:56 Type
2500testdata/Builtins.lc 504:49-504:50 V1 2474testdata/Builtins.lc 504:49-504:50 V1
2501testdata/Builtins.lc 504:51-504:56 Type 2475testdata/Builtins.lc 504:51-504:56 Type
2502testdata/Builtins.lc 504:61-504:62 Type 2476testdata/Builtins.lc 504:61-504:62 Type
2503testdata/Builtins.lc 504:61-504:72 Type 2477testdata/Builtins.lc 504:61-504:77 Type
2504testdata/Builtins.lc 504:66-504:67 Type 2478testdata/Builtins.lc 504:66-504:67 Type
2505testdata/Builtins.lc 504:66-504:72 Type 2479testdata/Builtins.lc 504:66-504:77 Type
2506testdata/Builtins.lc 504:71-504:72 Type 2480testdata/Builtins.lc 504:71-504:72 Type
2507testdata/Builtins.lc 506:1-506:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c 2481testdata/Builtins.lc 504:71-504:77 Type
2508testdata/Builtins.lc 506:34-506:37 Nat -> Nat -> Type->Type 2482testdata/Builtins.lc 504:76-504:77 Type
2509testdata/Builtins.lc 506:34-506:39 Nat -> Type->Type 2483testdata/Builtins.lc 505:1-505:12 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
2510testdata/Builtins.lc 506:34-506:41 Type->Type 2484testdata/Builtins.lc 505:34-505:57 Type
2511testdata/Builtins.lc 506:34-506:43 Type 2485testdata/Builtins.lc 505:34-505:72 Type
2512testdata/Builtins.lc 506:34-506:56 Type 2486testdata/Builtins.lc 505:35-505:36 V3
2513testdata/Builtins.lc 506:38-506:39 V5 2487testdata/Builtins.lc 505:35-505:38 Type->Type
2514testdata/Builtins.lc 506:40-506:41 V3 2488testdata/Builtins.lc 505:37-505:38 Type -> Type->Type
2515testdata/Builtins.lc 506:42-506:43 V1 2489testdata/Builtins.lc 505:39-505:48 Nat -> Type->Type
2516testdata/Builtins.lc 506:47-506:50 Nat -> Nat -> Type->Type 2490testdata/Builtins.lc 505:39-505:50 Type->Type
2517testdata/Builtins.lc 506:47-506:52 Nat -> Type->Type 2491testdata/Builtins.lc 505:39-505:56 Type
2518testdata/Builtins.lc 506:47-506:54 Type->Type 2492testdata/Builtins.lc 505:49-505:50 V1
2519testdata/Builtins.lc 506:47-506:56 Type 2493testdata/Builtins.lc 505:51-505:56 Type
2520testdata/Builtins.lc 506:51-506:52 Nat 2494testdata/Builtins.lc 505:61-505:62 Type
2521testdata/Builtins.lc 506:53-506:54 Nat 2495testdata/Builtins.lc 505:61-505:72 Type
2522testdata/Builtins.lc 506:55-506:56 Type 2496testdata/Builtins.lc 505:66-505:67 Type
2523testdata/Builtins.lc 507:1-507:16 {a:Nat} -> {b} -> Mat a a b -> Float 2497testdata/Builtins.lc 505:66-505:72 Type
2498testdata/Builtins.lc 505:71-505:72 Type
2499testdata/Builtins.lc 507:1-507:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c
2524testdata/Builtins.lc 507:34-507:37 Nat -> Nat -> Type->Type 2500testdata/Builtins.lc 507:34-507:37 Nat -> Nat -> Type->Type
2525testdata/Builtins.lc 507:34-507:39 Nat -> Type->Type 2501testdata/Builtins.lc 507:34-507:39 Nat -> Type->Type
2526testdata/Builtins.lc 507:34-507:41 Type->Type 2502testdata/Builtins.lc 507:34-507:41 Type->Type
2527testdata/Builtins.lc 507:34-507:43 Type 2503testdata/Builtins.lc 507:34-507:43 Type
2528testdata/Builtins.lc 507:34-507:52 Type 2504testdata/Builtins.lc 507:34-507:56 Type
2529testdata/Builtins.lc 507:38-507:39 V3 2505testdata/Builtins.lc 507:38-507:39 V5
2530testdata/Builtins.lc 507:40-507:41 Nat 2506testdata/Builtins.lc 507:40-507:41 V3
2531testdata/Builtins.lc 507:42-507:43 V1 2507testdata/Builtins.lc 507:42-507:43 V1
2532testdata/Builtins.lc 507:47-507:52 Type 2508testdata/Builtins.lc 507:47-507:50 Nat -> Nat -> Type->Type
2533testdata/Builtins.lc 508:1-508:12 {a:Nat} -> {b} -> Mat a a b -> Mat a a b 2509testdata/Builtins.lc 507:47-507:52 Nat -> Type->Type
2510testdata/Builtins.lc 507:47-507:54 Type->Type
2511testdata/Builtins.lc 507:47-507:56 Type
2512testdata/Builtins.lc 507:51-507:52 Nat
2513testdata/Builtins.lc 507:53-507:54 Nat
2514testdata/Builtins.lc 507:55-507:56 Type
2515testdata/Builtins.lc 508:1-508:16 {a:Nat} -> {b} -> Mat a a b -> Float
2534testdata/Builtins.lc 508:34-508:37 Nat -> Nat -> Type->Type 2516testdata/Builtins.lc 508:34-508:37 Nat -> Nat -> Type->Type
2535testdata/Builtins.lc 508:34-508:39 Nat -> Type->Type 2517testdata/Builtins.lc 508:34-508:39 Nat -> Type->Type
2536testdata/Builtins.lc 508:34-508:41 Type->Type 2518testdata/Builtins.lc 508:34-508:41 Type->Type
2537testdata/Builtins.lc 508:34-508:43 Type 2519testdata/Builtins.lc 508:34-508:43 Type
2538testdata/Builtins.lc 508:34-508:56 Type 2520testdata/Builtins.lc 508:34-508:52 Type
2539testdata/Builtins.lc 508:38-508:39 V3 2521testdata/Builtins.lc 508:38-508:39 V3
2540testdata/Builtins.lc 508:40-508:41 Nat 2522testdata/Builtins.lc 508:40-508:41 Nat
2541testdata/Builtins.lc 508:42-508:43 V1 2523testdata/Builtins.lc 508:42-508:43 V1
2542testdata/Builtins.lc 508:47-508:50 Nat -> Nat -> Type->Type 2524testdata/Builtins.lc 508:47-508:52 Type
2543testdata/Builtins.lc 508:47-508:52 Nat -> Type->Type 2525testdata/Builtins.lc 509:1-509:12 {a:Nat} -> {b} -> Mat a a b -> Mat a a b
2544testdata/Builtins.lc 508:47-508:54 Type->Type 2526testdata/Builtins.lc 509:34-509:37 Nat -> Nat -> Type->Type
2545testdata/Builtins.lc 508:47-508:56 Type 2527testdata/Builtins.lc 509:34-509:39 Nat -> Type->Type
2546testdata/Builtins.lc 508:51-508:52 Nat 2528testdata/Builtins.lc 509:34-509:41 Type->Type
2547testdata/Builtins.lc 508:53-508:54 Nat 2529testdata/Builtins.lc 509:34-509:43 Type
2548testdata/Builtins.lc 508:55-508:56 Type 2530testdata/Builtins.lc 509:34-509:56 Type
2549testdata/Builtins.lc 509:1-509:17 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> VecS b c -> Mat c a b 2531testdata/Builtins.lc 509:38-509:39 V3
2550testdata/Builtins.lc 509:34-509:37 Nat -> Type->Type 2532testdata/Builtins.lc 509:40-509:41 Nat
2551testdata/Builtins.lc 509:34-509:39 Type->Type 2533testdata/Builtins.lc 509:42-509:43 V1
2552testdata/Builtins.lc 509:34-509:41 Type 2534testdata/Builtins.lc 509:47-509:50 Nat -> Nat -> Type->Type
2553testdata/Builtins.lc 509:34-509:69 Type 2535testdata/Builtins.lc 509:47-509:52 Nat -> Type->Type
2554testdata/Builtins.lc 509:38-509:39 V5 2536testdata/Builtins.lc 509:47-509:54 Type->Type
2555testdata/Builtins.lc 509:40-509:41 V3 2537testdata/Builtins.lc 509:47-509:56 Type
2556testdata/Builtins.lc 509:47-509:50 Nat -> Type->Type 2538testdata/Builtins.lc 509:51-509:52 Nat
2557testdata/Builtins.lc 509:47-509:52 Type->Type 2539testdata/Builtins.lc 509:53-509:54 Nat
2558testdata/Builtins.lc 509:47-509:54 Type 2540testdata/Builtins.lc 509:55-509:56 Type
2559testdata/Builtins.lc 509:47-509:69 Type 2541testdata/Builtins.lc 510:1-510:17 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> VecS b c -> Mat c a b
2560testdata/Builtins.lc 509:51-509:52 V2 2542testdata/Builtins.lc 510:34-510:37 Nat -> Type->Type
2561testdata/Builtins.lc 509:53-509:54 Type 2543testdata/Builtins.lc 510:34-510:39 Type->Type
2562testdata/Builtins.lc 509:60-509:63 Nat -> Nat -> Type->Type 2544testdata/Builtins.lc 510:34-510:41 Type
2563testdata/Builtins.lc 509:60-509:65 Nat -> Type->Type 2545testdata/Builtins.lc 510:34-510:69 Type
2564testdata/Builtins.lc 509:60-509:67 Type->Type
2565testdata/Builtins.lc 509:60-509:69 Type
2566testdata/Builtins.lc 509:64-509:65 Nat
2567testdata/Builtins.lc 509:66-509:67 Nat
2568testdata/Builtins.lc 509:68-509:69 Type
2569testdata/Builtins.lc 510:1-510:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> VecS c b -> VecS c a
2570testdata/Builtins.lc 510:34-510:37 Nat -> Nat -> Type->Type
2571testdata/Builtins.lc 510:34-510:39 Nat -> Type->Type
2572testdata/Builtins.lc 510:34-510:41 Type->Type
2573testdata/Builtins.lc 510:34-510:43 Type
2574testdata/Builtins.lc 510:34-510:67 Type
2575testdata/Builtins.lc 510:38-510:39 V5 2546testdata/Builtins.lc 510:38-510:39 V5
2576testdata/Builtins.lc 510:40-510:41 V3 2547testdata/Builtins.lc 510:40-510:41 V3
2577testdata/Builtins.lc 510:42-510:43 V1
2578testdata/Builtins.lc 510:47-510:50 Nat -> Type->Type 2548testdata/Builtins.lc 510:47-510:50 Nat -> Type->Type
2579testdata/Builtins.lc 510:47-510:52 Type->Type 2549testdata/Builtins.lc 510:47-510:52 Type->Type
2580testdata/Builtins.lc 510:47-510:54 Type 2550testdata/Builtins.lc 510:47-510:54 Type
2581testdata/Builtins.lc 510:47-510:67 Type 2551testdata/Builtins.lc 510:47-510:69 Type
2582testdata/Builtins.lc 510:51-510:52 Nat 2552testdata/Builtins.lc 510:51-510:52 V2
2583testdata/Builtins.lc 510:53-510:54 Type 2553testdata/Builtins.lc 510:53-510:54 Type
2584testdata/Builtins.lc 510:60-510:63 Nat -> Type->Type 2554testdata/Builtins.lc 510:60-510:63 Nat -> Nat -> Type->Type
2585testdata/Builtins.lc 510:60-510:65 Type->Type 2555testdata/Builtins.lc 510:60-510:65 Nat -> Type->Type
2586testdata/Builtins.lc 510:60-510:67 Type 2556testdata/Builtins.lc 510:60-510:67 Type->Type
2557testdata/Builtins.lc 510:60-510:69 Type
2587testdata/Builtins.lc 510:64-510:65 Nat 2558testdata/Builtins.lc 510:64-510:65 Nat
2588testdata/Builtins.lc 510:66-510:67 Type 2559testdata/Builtins.lc 510:66-510:67 Nat
2589testdata/Builtins.lc 511:1-511:14 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> Mat a c b -> VecS b c 2560testdata/Builtins.lc 510:68-510:69 Type
2590testdata/Builtins.lc 511:34-511:37 Nat -> Type->Type 2561testdata/Builtins.lc 511:1-511:14 {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> VecS c b -> VecS c a
2591testdata/Builtins.lc 511:34-511:39 Type->Type 2562testdata/Builtins.lc 511:34-511:37 Nat -> Nat -> Type->Type
2592testdata/Builtins.lc 511:34-511:41 Type 2563testdata/Builtins.lc 511:34-511:39 Nat -> Type->Type
2564testdata/Builtins.lc 511:34-511:41 Type->Type
2565testdata/Builtins.lc 511:34-511:43 Type
2593testdata/Builtins.lc 511:34-511:67 Type 2566testdata/Builtins.lc 511:34-511:67 Type
2594testdata/Builtins.lc 511:38-511:39 V5 2567testdata/Builtins.lc 511:38-511:39 V5
2595testdata/Builtins.lc 511:40-511:41 V3 2568testdata/Builtins.lc 511:40-511:41 V3
2596testdata/Builtins.lc 511:47-511:50 Nat -> Nat -> Type->Type 2569testdata/Builtins.lc 511:42-511:43 V1
2597testdata/Builtins.lc 511:47-511:52 Nat -> Type->Type 2570testdata/Builtins.lc 511:47-511:50 Nat -> Type->Type
2598testdata/Builtins.lc 511:47-511:54 Type->Type 2571testdata/Builtins.lc 511:47-511:52 Type->Type
2599testdata/Builtins.lc 511:47-511:56 Type 2572testdata/Builtins.lc 511:47-511:54 Type
2600testdata/Builtins.lc 511:47-511:67 Type 2573testdata/Builtins.lc 511:47-511:67 Type
2601testdata/Builtins.lc 511:51-511:52 Nat 2574testdata/Builtins.lc 511:51-511:52 Nat
2602testdata/Builtins.lc 511:53-511:54 V2 2575testdata/Builtins.lc 511:53-511:54 Type
2603testdata/Builtins.lc 511:55-511:56 Type
2604testdata/Builtins.lc 511:60-511:63 Nat -> Type->Type 2576testdata/Builtins.lc 511:60-511:63 Nat -> Type->Type
2605testdata/Builtins.lc 511:60-511:65 Type->Type 2577testdata/Builtins.lc 511:60-511:65 Type->Type
2606testdata/Builtins.lc 511:60-511:67 Type 2578testdata/Builtins.lc 511:60-511:67 Type
2607testdata/Builtins.lc 511:64-511:65 Nat 2579testdata/Builtins.lc 511:64-511:65 Nat
2608testdata/Builtins.lc 511:66-511:67 Type 2580testdata/Builtins.lc 511:66-511:67 Type
2609testdata/Builtins.lc 512:1-512:14 {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c 2581testdata/Builtins.lc 512:1-512:14 {a:Nat} -> {b} -> {c:Nat} -> VecS b a -> Mat a c b -> VecS b c
2610testdata/Builtins.lc 512:34-512:37 Nat -> Nat -> Type->Type 2582testdata/Builtins.lc 512:34-512:37 Nat -> Type->Type
2611testdata/Builtins.lc 512:34-512:39 Nat -> Type->Type 2583testdata/Builtins.lc 512:34-512:39 Type->Type
2612testdata/Builtins.lc 512:34-512:41 Type->Type 2584testdata/Builtins.lc 512:34-512:41 Type
2613testdata/Builtins.lc 512:34-512:43 Type 2585testdata/Builtins.lc 512:34-512:67 Type
2614testdata/Builtins.lc 512:34-512:69 Type 2586testdata/Builtins.lc 512:38-512:39 V5
2615testdata/Builtins.lc 512:38-512:39 V7 2587testdata/Builtins.lc 512:40-512:41 V3
2616testdata/Builtins.lc 512:40-512:41 V5
2617testdata/Builtins.lc 512:42-512:43 V3
2618testdata/Builtins.lc 512:47-512:50 Nat -> Nat -> Type->Type 2588testdata/Builtins.lc 512:47-512:50 Nat -> Nat -> Type->Type
2619testdata/Builtins.lc 512:47-512:52 Nat -> Type->Type 2589testdata/Builtins.lc 512:47-512:52 Nat -> Type->Type
2620testdata/Builtins.lc 512:47-512:54 Type->Type 2590testdata/Builtins.lc 512:47-512:54 Type->Type
2621testdata/Builtins.lc 512:47-512:56 Type 2591testdata/Builtins.lc 512:47-512:56 Type
2622testdata/Builtins.lc 512:47-512:69 Type 2592testdata/Builtins.lc 512:47-512:67 Type
2623testdata/Builtins.lc 512:51-512:52 Nat 2593testdata/Builtins.lc 512:51-512:52 Nat
2624testdata/Builtins.lc 512:53-512:54 V2 2594testdata/Builtins.lc 512:53-512:54 V2
2625testdata/Builtins.lc 512:55-512:56 Type 2595testdata/Builtins.lc 512:55-512:56 Type
2626testdata/Builtins.lc 512:60-512:63 Nat -> Nat -> Type->Type 2596testdata/Builtins.lc 512:60-512:63 Nat -> Type->Type
2627testdata/Builtins.lc 512:60-512:65 Nat -> Type->Type 2597testdata/Builtins.lc 512:60-512:65 Type->Type
2628testdata/Builtins.lc 512:60-512:67 Type->Type 2598testdata/Builtins.lc 512:60-512:67 Type
2629testdata/Builtins.lc 512:60-512:69 Type
2630testdata/Builtins.lc 512:64-512:65 Nat 2599testdata/Builtins.lc 512:64-512:65 Nat
2631testdata/Builtins.lc 512:66-512:67 Nat 2600testdata/Builtins.lc 512:66-512:67 Type
2632testdata/Builtins.lc 512:68-512:69 Type 2601testdata/Builtins.lc 513:1-513:14 {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
2633testdata/Builtins.lc 514:1-514:13 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2602testdata/Builtins.lc 513:34-513:37 Nat -> Nat -> Type->Type
2634testdata/Builtins.lc 514:15-514:32 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2603testdata/Builtins.lc 513:34-513:39 Nat -> Type->Type
2635testdata/Builtins.lc 514:34-514:49 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2604testdata/Builtins.lc 513:34-513:41 Type->Type
2636testdata/Builtins.lc 514:51-514:71 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2605testdata/Builtins.lc 513:34-513:43 Type
2637testdata/Builtins.lc 514:73-514:83 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2606testdata/Builtins.lc 513:34-513:69 Type
2638testdata/Builtins.lc 514:85-514:98 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d 2607testdata/Builtins.lc 513:38-513:39 V7
2639testdata/Builtins.lc 515:34-515:97 Type 2608testdata/Builtins.lc 513:40-513:41 V5
2640testdata/Builtins.lc 515:35-515:38 Type->Type 2609testdata/Builtins.lc 513:42-513:43 V3
2641testdata/Builtins.lc 515:35-515:40 Type 2610testdata/Builtins.lc 513:47-513:50 Nat -> Nat -> Type->Type
2642testdata/Builtins.lc 515:39-515:40 V7 2611testdata/Builtins.lc 513:47-513:52 Nat -> Type->Type
2643testdata/Builtins.lc 515:42-515:43 V6 2612testdata/Builtins.lc 513:47-513:54 Type->Type
2644testdata/Builtins.lc 515:42-515:45 Type->Type 2613testdata/Builtins.lc 513:47-513:56 Type
2645testdata/Builtins.lc 515:42-515:59 Type 2614testdata/Builtins.lc 513:47-513:69 Type
2646testdata/Builtins.lc 515:42-515:97 Type 2615testdata/Builtins.lc 513:51-513:52 Nat
2647testdata/Builtins.lc 515:44-515:45 Type -> Type->Type 2616testdata/Builtins.lc 513:53-513:54 V2
2648testdata/Builtins.lc 515:46-515:55 Nat -> Type->Type 2617testdata/Builtins.lc 513:55-513:56 Type
2649testdata/Builtins.lc 515:46-515:57 Type->Type 2618testdata/Builtins.lc 513:60-513:63 Nat -> Nat -> Type->Type
2650testdata/Builtins.lc 515:46-515:59 Type 2619testdata/Builtins.lc 513:60-513:65 Nat -> Type->Type
2651testdata/Builtins.lc 515:56-515:57 V4 2620testdata/Builtins.lc 513:60-513:67 Type->Type
2652testdata/Builtins.lc 515:58-515:59 Type 2621testdata/Builtins.lc 513:60-513:69 Type
2653testdata/Builtins.lc 515:61-515:62 V3 2622testdata/Builtins.lc 513:64-513:65 Nat
2654testdata/Builtins.lc 515:61-515:64 Type->Type 2623testdata/Builtins.lc 513:66-513:67 Nat
2655testdata/Builtins.lc 515:61-515:81 Type 2624testdata/Builtins.lc 513:68-513:69 Type
2656testdata/Builtins.lc 515:61-515:97 Type 2625testdata/Builtins.lc 515:1-515:13 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2657testdata/Builtins.lc 515:63-515:64 Type -> Type->Type 2626testdata/Builtins.lc 515:15-515:32 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2658testdata/Builtins.lc 515:65-515:74 Nat -> Type->Type 2627testdata/Builtins.lc 515:34-515:49 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2659testdata/Builtins.lc 515:65-515:76 Type->Type 2628testdata/Builtins.lc 515:51-515:71 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2660testdata/Builtins.lc 515:65-515:81 Type 2629testdata/Builtins.lc 515:73-515:83 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2661testdata/Builtins.lc 515:75-515:76 Nat 2630testdata/Builtins.lc 515:85-515:98 {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
2662testdata/Builtins.lc 515:77-515:81 Type 2631testdata/Builtins.lc 516:34-516:97 Type
2663testdata/Builtins.lc 515:86-515:87 Type
2664testdata/Builtins.lc 515:86-515:97 Type
2665testdata/Builtins.lc 515:91-515:92 Type
2666testdata/Builtins.lc 515:91-515:97 Type
2667testdata/Builtins.lc 515:96-515:97 Type
2668testdata/Builtins.lc 516:1-516:10 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
2669testdata/Builtins.lc 516:12-516:24 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
2670testdata/Builtins.lc 516:34-516:58 Type
2671testdata/Builtins.lc 516:34-516:76 Type
2672testdata/Builtins.lc 516:35-516:36 V3
2673testdata/Builtins.lc 516:35-516:38 Type->Type 2632testdata/Builtins.lc 516:35-516:38 Type->Type
2674testdata/Builtins.lc 516:37-516:38 Type -> Type->Type 2633testdata/Builtins.lc 516:35-516:40 Type
2675testdata/Builtins.lc 516:39-516:55 Type->Type 2634testdata/Builtins.lc 516:39-516:40 V7
2676testdata/Builtins.lc 516:39-516:57 Type 2635testdata/Builtins.lc 516:42-516:43 V6
2677testdata/Builtins.lc 516:56-516:57 V1 2636testdata/Builtins.lc 516:42-516:45 Type->Type
2678testdata/Builtins.lc 516:62-516:63 Type 2637testdata/Builtins.lc 516:42-516:59 Type
2679testdata/Builtins.lc 516:62-516:76 Type 2638testdata/Builtins.lc 516:42-516:97 Type
2680testdata/Builtins.lc 516:67-516:68 Type 2639testdata/Builtins.lc 516:44-516:45 Type -> Type->Type
2681testdata/Builtins.lc 516:67-516:76 Type 2640testdata/Builtins.lc 516:46-516:55 Nat -> Type->Type
2682testdata/Builtins.lc 516:72-516:76 Type 2641testdata/Builtins.lc 516:46-516:57 Type->Type
2683testdata/Builtins.lc 518:1-518:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2642testdata/Builtins.lc 516:46-516:59 Type
2684testdata/Builtins.lc 518:11-518:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2643testdata/Builtins.lc 516:56-516:57 V4
2685testdata/Builtins.lc 518:21-518:31 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a 2644testdata/Builtins.lc 516:58-516:59 Type
2686testdata/Builtins.lc 519:34-519:57 Type 2645testdata/Builtins.lc 516:61-516:62 V3
2687testdata/Builtins.lc 519:34-519:67 Type 2646testdata/Builtins.lc 516:61-516:64 Type->Type
2688testdata/Builtins.lc 519:35-519:36 V3 2647testdata/Builtins.lc 516:61-516:81 Type
2689testdata/Builtins.lc 519:35-519:38 Type->Type 2648testdata/Builtins.lc 516:61-516:97 Type
2690testdata/Builtins.lc 519:37-519:38 Type -> Type->Type 2649testdata/Builtins.lc 516:63-516:64 Type -> Type->Type
2691testdata/Builtins.lc 519:39-519:48 Nat -> Type->Type 2650testdata/Builtins.lc 516:65-516:74 Nat -> Type->Type
2692testdata/Builtins.lc 519:39-519:50 Type->Type 2651testdata/Builtins.lc 516:65-516:76 Type->Type
2693testdata/Builtins.lc 519:39-519:56 Type 2652testdata/Builtins.lc 516:65-516:81 Type
2694testdata/Builtins.lc 519:49-519:50 V1 2653testdata/Builtins.lc 516:75-516:76 Nat
2695testdata/Builtins.lc 519:51-519:56 Type 2654testdata/Builtins.lc 516:77-516:81 Type
2696testdata/Builtins.lc 519:61-519:62 Type 2655testdata/Builtins.lc 516:86-516:87 Type
2697testdata/Builtins.lc 519:61-519:67 Type 2656testdata/Builtins.lc 516:86-516:97 Type
2698testdata/Builtins.lc 519:66-519:67 Type 2657testdata/Builtins.lc 516:91-516:92 Type
2699testdata/Builtins.lc 521:1-521:11 {a:Nat} -> VecScalar a Float -> Float 2658testdata/Builtins.lc 516:91-516:97 Type
2700testdata/Builtins.lc 521:34-521:43 Nat -> Type->Type 2659testdata/Builtins.lc 516:96-516:97 Type
2701testdata/Builtins.lc 521:34-521:45 Type->Type 2660testdata/Builtins.lc 517:1-517:10 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
2702testdata/Builtins.lc 521:34-521:51 Type 2661testdata/Builtins.lc 517:12-517:24 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
2703testdata/Builtins.lc 521:34-521:60 Type 2662testdata/Builtins.lc 517:34-517:58 Type
2704testdata/Builtins.lc 521:44-521:45 V1 2663testdata/Builtins.lc 517:34-517:76 Type
2705testdata/Builtins.lc 521:46-521:51 Type 2664testdata/Builtins.lc 517:35-517:36 V3
2706testdata/Builtins.lc 521:55-521:60 Type 2665testdata/Builtins.lc 517:35-517:38 Type->Type
2707testdata/Builtins.lc 522:1-522:11 {a:Nat} -> VecScalar a Float -> VecS Float 2 2666testdata/Builtins.lc 517:37-517:38 Type -> Type->Type
2667testdata/Builtins.lc 517:39-517:55 Type->Type
2668testdata/Builtins.lc 517:39-517:57 Type
2669testdata/Builtins.lc 517:56-517:57 V1
2670testdata/Builtins.lc 517:62-517:63 Type
2671testdata/Builtins.lc 517:62-517:76 Type
2672testdata/Builtins.lc 517:67-517:68 Type
2673testdata/Builtins.lc 517:67-517:76 Type
2674testdata/Builtins.lc 517:72-517:76 Type
2675testdata/Builtins.lc 519:1-519:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2676testdata/Builtins.lc 519:11-519:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2677testdata/Builtins.lc 519:21-519:31 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
2678testdata/Builtins.lc 520:34-520:57 Type
2679testdata/Builtins.lc 520:34-520:67 Type
2680testdata/Builtins.lc 520:35-520:36 V3
2681testdata/Builtins.lc 520:35-520:38 Type->Type
2682testdata/Builtins.lc 520:37-520:38 Type -> Type->Type
2683testdata/Builtins.lc 520:39-520:48 Nat -> Type->Type
2684testdata/Builtins.lc 520:39-520:50 Type->Type
2685testdata/Builtins.lc 520:39-520:56 Type
2686testdata/Builtins.lc 520:49-520:50 V1
2687testdata/Builtins.lc 520:51-520:56 Type
2688testdata/Builtins.lc 520:61-520:62 Type
2689testdata/Builtins.lc 520:61-520:67 Type
2690testdata/Builtins.lc 520:66-520:67 Type
2691testdata/Builtins.lc 522:1-522:11 {a:Nat} -> VecScalar a Float -> Float
2708testdata/Builtins.lc 522:34-522:43 Nat -> Type->Type 2692testdata/Builtins.lc 522:34-522:43 Nat -> Type->Type
2709testdata/Builtins.lc 522:34-522:45 Type->Type 2693testdata/Builtins.lc 522:34-522:45 Type->Type
2710testdata/Builtins.lc 522:34-522:51 Type 2694testdata/Builtins.lc 522:34-522:51 Type
2711testdata/Builtins.lc 522:34-522:66 Type 2695testdata/Builtins.lc 522:34-522:60 Type
2712testdata/Builtins.lc 522:44-522:45 V1 2696testdata/Builtins.lc 522:44-522:45 V1
2713testdata/Builtins.lc 522:46-522:51 Type 2697testdata/Builtins.lc 522:46-522:51 Type
2714testdata/Builtins.lc 522:55-522:58 Nat -> Type->Type 2698testdata/Builtins.lc 522:55-522:60 Type
2715testdata/Builtins.lc 522:55-522:60 Type->Type 2699testdata/Builtins.lc 523:1-523:11 {a:Nat} -> VecScalar a Float -> VecS Float 2
2716testdata/Builtins.lc 522:55-522:66 Type
2717testdata/Builtins.lc 522:59-522:60 V1
2718testdata/Builtins.lc 522:61-522:66 Type
2719testdata/Builtins.lc 523:1-523:11 {a:Nat} -> VecScalar a Float -> VecS Float 3
2720testdata/Builtins.lc 523:34-523:43 Nat -> Type->Type 2700testdata/Builtins.lc 523:34-523:43 Nat -> Type->Type
2721testdata/Builtins.lc 523:34-523:45 Type->Type 2701testdata/Builtins.lc 523:34-523:45 Type->Type
2722testdata/Builtins.lc 523:34-523:51 Type 2702testdata/Builtins.lc 523:34-523:51 Type
@@ -2728,7 +2708,7 @@ testdata/Builtins.lc 523:55-523:60 Type->Type
2728testdata/Builtins.lc 523:55-523:66 Type 2708testdata/Builtins.lc 523:55-523:66 Type
2729testdata/Builtins.lc 523:59-523:60 V1 2709testdata/Builtins.lc 523:59-523:60 V1
2730testdata/Builtins.lc 523:61-523:66 Type 2710testdata/Builtins.lc 523:61-523:66 Type
2731testdata/Builtins.lc 524:1-524:11 {a:Nat} -> VecScalar a Float -> VecS Float 4 2711testdata/Builtins.lc 524:1-524:11 {a:Nat} -> VecScalar a Float -> VecS Float 3
2732testdata/Builtins.lc 524:34-524:43 Nat -> Type->Type 2712testdata/Builtins.lc 524:34-524:43 Nat -> Type->Type
2733testdata/Builtins.lc 524:34-524:45 Type->Type 2713testdata/Builtins.lc 524:34-524:45 Type->Type
2734testdata/Builtins.lc 524:34-524:51 Type 2714testdata/Builtins.lc 524:34-524:51 Type
@@ -2740,82 +2720,94 @@ testdata/Builtins.lc 524:55-524:60 Type->Type
2740testdata/Builtins.lc 524:55-524:66 Type 2720testdata/Builtins.lc 524:55-524:66 Type
2741testdata/Builtins.lc 524:59-524:60 V1 2721testdata/Builtins.lc 524:59-524:60 V1
2742testdata/Builtins.lc 524:61-524:66 Type 2722testdata/Builtins.lc 524:61-524:66 Type
2743testdata/Builtins.lc 540:6-540:13 Type 2723testdata/Builtins.lc 525:1-525:11 {a:Nat} -> VecScalar a Float -> VecS Float 4
2744testdata/Builtins.lc 540:6-544:12 Type 2724testdata/Builtins.lc 525:34-525:43 Nat -> Type->Type
2745testdata/Builtins.lc 541:3-541:16 String->Texture | Texture | Type 2725testdata/Builtins.lc 525:34-525:45 Type->Type
2746testdata/Builtins.lc 541:20-541:26 Type 2726testdata/Builtins.lc 525:34-525:51 Type
2747testdata/Builtins.lc 542:20-542:27 Type 2727testdata/Builtins.lc 525:34-525:66 Type
2748testdata/Builtins.lc 544:3-544:12 Texture | Type | VecS Int 2 -> Image 1 (Color (VecS Float 4)) -> Texture 2728testdata/Builtins.lc 525:44-525:45 V1
2749testdata/Builtins.lc 544:20-544:23 Nat -> Type->Type 2729testdata/Builtins.lc 525:46-525:51 Type
2750testdata/Builtins.lc 544:20-544:25 Type->Type 2730testdata/Builtins.lc 525:55-525:58 Nat -> Type->Type
2751testdata/Builtins.lc 544:20-544:29 Type 2731testdata/Builtins.lc 525:55-525:60 Type->Type
2752testdata/Builtins.lc 544:24-544:25 V1 2732testdata/Builtins.lc 525:55-525:66 Type
2753testdata/Builtins.lc 544:26-544:29 Type 2733testdata/Builtins.lc 525:59-525:60 V1
2754testdata/Builtins.lc 545:20-545:25 Nat -> Type->Type 2734testdata/Builtins.lc 525:61-525:66 Type
2755testdata/Builtins.lc 545:20-545:27 Type->Type 2735testdata/Builtins.lc 541:6-541:13 Type
2756testdata/Builtins.lc 545:20-545:49 Type 2736testdata/Builtins.lc 541:6-545:12 Type
2757testdata/Builtins.lc 545:20-546:27 Type 2737testdata/Builtins.lc 542:3-542:16 String->Texture | Texture | Type
2758testdata/Builtins.lc 545:26-545:27 V1 2738testdata/Builtins.lc 542:20-542:26 Type
2759testdata/Builtins.lc 545:28-545:49 Type 2739testdata/Builtins.lc 543:20-543:27 Type
2760testdata/Builtins.lc 545:29-545:34 Type->Type 2740testdata/Builtins.lc 545:3-545:12 Texture | Type | VecS Int 2 -> Image 1 (Color (VecS Float 4)) -> Texture
2761testdata/Builtins.lc 545:35-545:48 Type 2741testdata/Builtins.lc 545:20-545:23 Nat -> Type->Type
2762testdata/Builtins.lc 545:36-545:39 Nat -> Type->Type 2742testdata/Builtins.lc 545:20-545:25 Type->Type
2763testdata/Builtins.lc 545:36-545:41 Type->Type 2743testdata/Builtins.lc 545:20-545:29 Type
2764testdata/Builtins.lc 545:40-545:41 V1 2744testdata/Builtins.lc 545:24-545:25 V1
2765testdata/Builtins.lc 545:42-545:47 Type 2745testdata/Builtins.lc 545:26-545:29 Type
2766testdata/Builtins.lc 546:20-546:27 Type 2746testdata/Builtins.lc 546:20-546:25 Nat -> Type->Type
2767testdata/Builtins.lc 548:6-548:12 Type 2747testdata/Builtins.lc 546:20-546:27 Type->Type
2768testdata/Builtins.lc 548:6-550:17 Type 2748testdata/Builtins.lc 546:20-546:49 Type
2769testdata/Builtins.lc 549:5-549:16 Filter 2749testdata/Builtins.lc 546:20-547:27 Type
2770testdata/Builtins.lc 550:5-550:17 Filter 2750testdata/Builtins.lc 546:26-546:27 V1
2771testdata/Builtins.lc 552:6-552:14 Type 2751testdata/Builtins.lc 546:28-546:49 Type
2772testdata/Builtins.lc 552:6-555:16 Type 2752testdata/Builtins.lc 546:29-546:34 Type->Type
2773testdata/Builtins.lc 553:5-553:11 EdgeMode 2753testdata/Builtins.lc 546:35-546:48 Type
2774testdata/Builtins.lc 554:5-554:19 EdgeMode 2754testdata/Builtins.lc 546:36-546:39 Nat -> Type->Type
2775testdata/Builtins.lc 555:5-555:16 EdgeMode 2755testdata/Builtins.lc 546:36-546:41 Type->Type
2776testdata/Builtins.lc 557:6-557:13 Type 2756testdata/Builtins.lc 546:40-546:41 V1
2777testdata/Builtins.lc 557:6-557:23 Type 2757testdata/Builtins.lc 546:42-546:47 Type
2778testdata/Builtins.lc 557:6-557:47 Type 2758testdata/Builtins.lc 547:20-547:27 Type
2779testdata/Builtins.lc 557:16-557:23 Filter -> EdgeMode -> Texture->Sampler | Sampler | Type 2759testdata/Builtins.lc 549:6-549:12 Type
2780testdata/Builtins.lc 557:24-557:30 Type 2760testdata/Builtins.lc 549:6-551:17 Type
2781testdata/Builtins.lc 557:31-557:39 Type 2761testdata/Builtins.lc 550:5-550:16 Filter
2782testdata/Builtins.lc 557:40-557:47 Type 2762testdata/Builtins.lc 551:5-551:17 Filter
2783testdata/Builtins.lc 560:1-560:10 Sampler -> VecS Float 2 -> VecS Float 4 2763testdata/Builtins.lc 553:6-553:14 Type
2784testdata/Builtins.lc 560:14-560:21 Type 2764testdata/Builtins.lc 553:6-556:16 Type
2785testdata/Builtins.lc 560:25-560:28 Nat -> Type->Type 2765testdata/Builtins.lc 554:5-554:11 EdgeMode
2786testdata/Builtins.lc 560:25-560:30 Type->Type 2766testdata/Builtins.lc 555:5-555:19 EdgeMode
2787testdata/Builtins.lc 560:25-560:36 Type 2767testdata/Builtins.lc 556:5-556:16 EdgeMode
2788testdata/Builtins.lc 560:25-560:51 Type 2768testdata/Builtins.lc 558:6-558:13 Type
2789testdata/Builtins.lc 560:29-560:30 V1 2769testdata/Builtins.lc 558:6-558:23 Type
2790testdata/Builtins.lc 560:31-560:36 Type 2770testdata/Builtins.lc 558:6-558:47 Type
2791testdata/Builtins.lc 560:40-560:43 Nat -> Type->Type 2771testdata/Builtins.lc 558:16-558:23 Filter -> EdgeMode -> Texture->Sampler | Sampler | Type
2792testdata/Builtins.lc 560:40-560:45 Type->Type 2772testdata/Builtins.lc 558:24-558:30 Type
2793testdata/Builtins.lc 560:40-560:51 Type 2773testdata/Builtins.lc 558:31-558:39 Type
2794testdata/Builtins.lc 560:44-560:45 V1 2774testdata/Builtins.lc 558:40-558:47 Type
2795testdata/Builtins.lc 560:46-560:51 Type 2775testdata/Builtins.lc 561:1-561:10 Sampler -> VecS Float 2 -> VecS Float 4
2796testdata/Builtins.lc 563:1-563:15 {a} -> {b} -> a -> b -> Tuple2 a b 2776testdata/Builtins.lc 561:14-561:21 Type
2797testdata/Builtins.lc 563:24-563:32 Tuple2 V3 V1 2777testdata/Builtins.lc 561:25-561:28 Nat -> Type->Type
2798testdata/Builtins.lc 563:25-563:28 V5 2778testdata/Builtins.lc 561:25-561:30 Type->Type
2799testdata/Builtins.lc 563:30-563:31 V2 2779testdata/Builtins.lc 561:25-561:36 Type
2800testdata/Builtins.lc 564:1-564:8 {a:Nat} -> {b} -> FrameBuffer a b -> Tuple2 (FragOps' b) (List (Vector a (Maybe (SimpleFragment (RemSemantics b))))) -> FrameBuffer a b 2780testdata/Builtins.lc 561:25-561:51 Type
2801testdata/Builtins.lc 564:13-564:21 V3 2781testdata/Builtins.lc 561:29-561:30 V1
2802testdata/Builtins.lc 564:13-564:46 FrameBuffer V1 V0 2782testdata/Builtins.lc 561:31-561:36 Type
2803testdata/Builtins.lc 564:25-564:35 {a:Nat} -> {b} -> FragOps' b -> List (Vector a (Maybe (SimpleFragment (RemSemantics b)))) -> FrameBuffer a b -> FrameBuffer a b 2783testdata/Builtins.lc 561:40-561:43 Nat -> Type->Type
2804testdata/Builtins.lc 564:25-564:39 List (Vector V1 (Maybe (SimpleFragment (RemSemantics V0)))) -> FrameBuffer V2 V1 -> FrameBuffer V3 V2 2784testdata/Builtins.lc 561:40-561:45 Type->Type
2805testdata/Builtins.lc 564:25-564:43 FrameBuffer V1 V0 -> FrameBuffer V2 V1 2785testdata/Builtins.lc 561:40-561:51 Type
2806testdata/Builtins.lc 564:25-564:46 FrameBuffer V1 V0 | V2 -> V2->V2 | V2->V2 2786testdata/Builtins.lc 561:44-561:45 V1
2807testdata/Builtins.lc 564:36-564:39 V6 2787testdata/Builtins.lc 561:46-561:51 Type
2808testdata/Builtins.lc 564:40-564:43 V5 2788testdata/Builtins.lc 564:1-564:15 {a} -> {b} -> a -> b -> Tuple2 a b
2809testdata/Builtins.lc 564:44-564:46 V7 2789testdata/Builtins.lc 564:24-564:32 Tuple2 V3 V1
2810testdata/Builtins.lc 565:1-565:12 {a:Nat} -> {b} -> FrameBuffer a b -> Output 2790testdata/Builtins.lc 564:25-564:28 V5
2811testdata/Builtins.lc 565:15-565:24 {a:Nat} -> {b} -> FrameBuffer a b -> Output 2791testdata/Builtins.lc 564:30-564:31 V2
2812testdata/Builtins.lc 566:1-566:11 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a 2792testdata/Builtins.lc 565:1-565:8 {a} -> {b:Nat} -> FrameBuffer b a -> Tuple2 (FragOps a) (List (Vector b (Maybe (SimpleFragment (RemSemantics a))))) -> FrameBuffer b a
2813testdata/Builtins.lc 566:14-566:25 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a 2793testdata/Builtins.lc 565:13-565:21 V3
2814testdata/Builtins.lc 567:1-567:16 Float -> Image 1 (Depth Float) 2794testdata/Builtins.lc 565:13-565:46 FrameBuffer V0 V1
2815testdata/Builtins.lc 567:19-567:29 {a:Nat} -> Float -> Image a (Depth Float) 2795testdata/Builtins.lc 565:25-565:35 {a} -> {b:Nat} -> FragOps a -> List (Vector b (Maybe (SimpleFragment (RemSemantics a)))) -> FrameBuffer b a -> FrameBuffer b a
2816testdata/Builtins.lc 567:19-567:32 Float -> Image 1 (Depth Float) 2796testdata/Builtins.lc 565:25-565:39 List (Vector V0 (Maybe (SimpleFragment (RemSemantics V1)))) -> FrameBuffer V1 V2 -> FrameBuffer V2 V3
2817testdata/Builtins.lc 567:31-567:32 V1 2797testdata/Builtins.lc 565:25-565:43 FrameBuffer V0 V1 -> FrameBuffer V1 V2
2818testdata/Builtins.lc 568:1-568:16 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) 2798testdata/Builtins.lc 565:25-565:46 FrameBuffer V0 V1 | V2 -> V2->V2 | V2->V2
2819testdata/Builtins.lc 568:19-568:29 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d) 2799testdata/Builtins.lc 565:36-565:39 V6
2820testdata/Builtins.lc 568:19-568:32 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c) 2800testdata/Builtins.lc 565:40-565:43 V5
2801testdata/Builtins.lc 565:44-565:46 V7
2802testdata/Builtins.lc 566:1-566:12 {a:Nat} -> {b} -> FrameBuffer a b -> Output
2803testdata/Builtins.lc 566:15-566:24 {a:Nat} -> {b} -> FrameBuffer a b -> Output
2804testdata/Builtins.lc 567:1-567:11 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a
2805testdata/Builtins.lc 567:14-567:25 {a} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a
2806testdata/Builtins.lc 568:1-568:16 Float -> Image 1 (Depth Float)
2807testdata/Builtins.lc 568:19-568:29 {a:Nat} -> Float -> Image a (Depth Float)
2808testdata/Builtins.lc 568:19-568:32 Float -> Image 1 (Depth Float)
2821testdata/Builtins.lc 568:31-568:32 V1 2809testdata/Builtins.lc 568:31-568:32 V1
2810testdata/Builtins.lc 569:1-569:16 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c)
2811testdata/Builtins.lc 569:19-569:29 {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a (Color d)
2812testdata/Builtins.lc 569:19-569:32 {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 (Color c)
2813testdata/Builtins.lc 569:31-569:32 V1
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 14:21:16 +0000