main is not found
------------ trace
id :: {a} -> a->a
'VecS :: Type -> 'Nat->Type
V2 :: {a} -> a -> a -> 'VecS a 2
V3 :: {a} -> a -> a -> a -> 'VecS a 3
V4 :: {a} -> a -> a -> a -> a -> 'VecS a 4
'VecSCase :: {a} -> (d : b:'Nat -> 'VecS a b -> Type) -> (e:a -> f:a -> d 2 (V2 e f)) -> (h:a -> i:a -> j:a -> d 3 (V3 h i j)) -> (l:a -> m:a -> n:a -> o:a -> d 4 (V4 l m n o)) -> {q:'Nat} -> (r : 'VecS a q) -> d q r
match'VecS :: (b : Type->Type) -> (c:Type -> d:'Nat -> b ('VecS c d)) -> f:Type -> b f -> b f
mapVec :: {a} -> {b} -> {c:'Nat} -> a->b -> 'VecS a c -> 'VecS b c
'Vec :: 'Nat -> Type->Type
'VecScalar :: 'Nat -> Type->Type
'Mat :: 'Nat -> 'Nat -> Type->Type
M22F :: 'Vec 2 'Float -> 'Vec 2 'Float -> 'Mat 2 2 'Float
M32F :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'Mat 3 2 'Float
M42F :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Mat 4 2 'Float
M23F :: 'Vec 2 'Float -> 'Vec 2 'Float -> 'Vec 2 'Float -> 'Mat 2 3 'Float
M33F :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'Vec 3 'Float -> 'Mat 3 3 'Float
M43F :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Mat 4 3 'Float
M24F :: 'Vec 2 'Float -> 'Vec 2 'Float -> 'Vec 2 'Float -> 'Vec 2 'Float -> 'Mat 2 4 'Float
M34F :: 'Vec 3 'Float -> 'Vec 3 'Float -> 'Vec 3 'Float -> 'Vec 3 'Float -> 'Mat 3 4 'Float
M44F :: 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Vec 4 'Float -> 'Mat 4 4 'Float
'MatCase :: (e : a:'Nat -> b:'Nat -> c:Type -> 'Mat a b c -> Type) -> ((f : 'Vec 2 'Float) -> (g : 'Vec 2 'Float) -> e 2 2 'Float (M22F f g)) -> ((i : 'Vec 3 'Float) -> (j : 'Vec 3 'Float) -> e 3 2 'Float (M32F i j)) -> ((l : 'Vec 4 'Float) -> (m : 'Vec 4 'Float) -> e 4 2 'Float (M42F l m)) -> ((o : 'Vec 2 'Float) -> (p : 'Vec 2 'Float) -> (q : 'Vec 2 'Float) -> e 2 3 'Float (M23F o p q)) -> ((s : 'Vec 3 'Float) -> (t : 'Vec 3 'Float) -> (u : 'Vec 3 'Float) -> e 3 3 'Float (M33F s t u)) -> ((w : 'Vec 4 'Float) -> (x : 'Vec 4 'Float) -> (y : 'Vec 4 'Float) -> e 4 3 'Float (M43F w x y)) -> ((a' : 'Vec 2 'Float) -> (b' : 'Vec 2 'Float) -> (c' : 'Vec 2 'Float) -> (d' : 'Vec 2 'Float) -> e 2 4 'Float (M24F a' b' c' d')) -> ((f' : 'Vec 3 'Float) -> (g' : 'Vec 3 'Float) -> (h' : 'Vec 3 'Float) -> (i' : 'Vec 3 'Float) -> e 3 4 'Float (M34F f' g' h' i')) -> ((k' : 'Vec 4 'Float) -> (l' : 'Vec 4 'Float) -> (m' : 'Vec 4 'Float) -> (n' : 'Vec 4 'Float) -> e 4 4 'Float (M44F k' l' m' n')) -> {p':'Nat} -> {q':'Nat} -> {r'} -> (s' : 'Mat p' q' r') -> e p' q' r' s'
match'Mat :: (b : Type->Type) -> (c:'Nat -> d:'Nat -> e:Type -> b ('Mat c d e)) -> g:Type -> b g -> b g
'MatVecScalarElem :: Type->Type
'Signed :: Type->Type
'Component :: Type->Type
zero :: {a} -> {b : 'Component a}->a
one :: {a} -> {b : 'Component a}->a
'Integral :: Type->Type
'Floating :: Type->Type
PrimAdd :: {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a
PrimSub :: {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a
PrimMul :: {a} -> {b : 'Num ('MatVecScalarElem a)} -> a -> a->a
PrimAddS :: {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b
PrimSubS :: {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b
PrimMulS :: {a} -> {b} -> {c : a ~ 'MatVecScalarElem b} -> {d : 'Num a} -> b -> a->b
PrimDiv :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimMod :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimDivS :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimModS :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimNeg :: {a} -> {b : 'Signed ('MatVecScalarElem a)} -> a->a
PrimBAnd :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimBOr :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimBXor :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimBAndS :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimBOrS :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimBXorS :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimBNot :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b->b
PrimBShiftL :: {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b
PrimBShiftR :: {a} -> {b} -> {c:'Nat} -> {d} -> {e : 'Integral a} -> {f : b ~ 'VecScalar c a} -> {g : d ~ 'VecScalar c 'Word} -> b -> d->b
PrimBShiftLS :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b
PrimBShiftRS :: {a} -> {b} -> {c:'Nat} -> {d : 'Integral a} -> {e : b ~ 'VecScalar c a} -> b -> 'Word->b
PrimAnd :: 'Bool -> 'Bool->'Bool
PrimOr :: 'Bool -> 'Bool->'Bool
PrimXor :: 'Bool -> 'Bool->'Bool
PrimNot :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Bool} -> a->a
PrimAny :: {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool
PrimAll :: {a:'Nat} -> 'VecScalar a 'Bool -> 'Bool
PrimACos :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimACosH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimASin :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimASinH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimATan :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimATanH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimCos :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimCosH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimDegrees :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimRadians :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimSin :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimSinH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimTan :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimTanH :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimExp :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimLog :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimExp2 :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimLog2 :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimSqrt :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimInvSqrt :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimPow :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a
PrimATan2 :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a
PrimFloor :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimTrunc :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimRound :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimRoundEven :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimCeil :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimFract :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimMin :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimMax :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b->b
PrimMinS :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimMaxS :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a->b
PrimIsNan :: {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c
PrimIsInf :: {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a->c
PrimAbs :: {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b
PrimSign :: {a} -> {b} -> {c:'Nat} -> {d : 'Signed a} -> {e : b ~ 'VecScalar c a} -> b->b
PrimModF :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->(a, a)
PrimClamp :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> b -> b->b
PrimClampS :: {a} -> {b} -> {c:'Nat} -> {d : 'Num a} -> {e : b ~ 'VecScalar c a} -> b -> a -> a->b
PrimMix :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a
PrimMixS :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> 'Float->a
PrimMixB :: {a} -> {b:'Nat} -> {c} -> {d : a ~ 'VecScalar b 'Float} -> {e : c ~ 'VecScalar b 'Bool} -> a -> a -> c->a
PrimStep :: {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a->a
PrimStepS :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> a->a
PrimSmoothStep :: {a} -> {b:'Nat} -> {c : a ~ 'VecS 'Float b} -> a -> a -> a->a
PrimSmoothStepS :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> 'Float -> 'Float -> a->a
PrimFloatBitsToInt :: {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Int
PrimFloatBitsToUInt :: {a:'Nat} -> 'VecScalar a 'Float -> 'VecScalar a 'Word
PrimIntBitsToFloat :: {a:'Nat} -> 'VecScalar a 'Int -> 'VecScalar a 'Float
PrimUIntBitsToFloat :: {a:'Nat} -> 'VecScalar a 'Word -> 'VecScalar a 'Float
PrimLength :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->'Float
PrimDistance :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float
PrimDot :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->'Float
PrimCross :: {a} -> {b : a ~ 'VecS 'Float 3} -> a -> a->a
PrimNormalize :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimFaceForward :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a
PrimRefract :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a -> a->a
PrimReflect :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a -> a->a
PrimTranspose :: {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Mat b a c
PrimDeterminant :: {a:'Nat} -> {b} -> 'Mat a a b -> 'Float
PrimInverse :: {a:'Nat} -> {b} -> 'Mat a a b -> 'Mat a a b
PrimOuterProduct :: {a:'Nat} -> {b} -> {c:'Nat} -> 'Vec a b -> 'Vec c b -> 'Mat c a b
PrimMulMatVec :: {a:'Nat} -> {b:'Nat} -> {c} -> 'Mat a b c -> 'Vec b c -> 'Vec a c
PrimMulVecMat :: {a:'Nat} -> {b} -> {c:'Nat} -> 'Vec a b -> 'Mat a c b -> 'Vec c b
PrimMulMatMat :: {a:'Nat} -> {b:'Nat} -> {c} -> {d:'Nat} -> 'Mat a b c -> 'Mat b d c -> 'Mat a d c
PrimLessThan :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimLessThanEqual :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimGreaterThan :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimGreaterThanEqual :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimEqualV :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimNotEqualV :: {a} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : a ~ 'VecScalar b c} -> {g : d ~ 'VecScalar b 'Bool} -> a -> a->d
PrimEqual :: {a} -> {b} -> {c : b ~ 'MatVecScalarElem a} -> a -> a->'Bool
PrimNotEqual :: {a} -> {b} -> {c : b ~ 'MatVecScalarElem a} -> a -> a->'Bool
PrimDFdx :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimDFdy :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimFWidth :: {a} -> {b:'Nat} -> {c : a ~ 'VecScalar b 'Float} -> a->a
PrimNoise1 :: {a:'Nat} -> 'VecScalar a 'Float -> 'Float
PrimNoise2 :: {a:'Nat} -> 'VecScalar a 'Float -> 'Vec 2 'Float
PrimNoise3 :: {a:'Nat} -> 'VecScalar a 'Float -> 'Vec 3 'Float
PrimNoise4 :: {a:'Nat} -> 'VecScalar a 'Float -> 'Vec 4 'Float
head :: {a} -> 'List a -> a
++ :: {a} -> 'List a -> 'List a -> 'List a
foldr :: {a} -> {b} -> (b -> a->a) -> a -> 'List b -> a
concat :: {a} -> 'List ('List a) -> 'List a
map :: {a} -> {b} -> a->b -> 'List a -> 'List b
concatMap :: {a} -> {b} -> (a -> 'List b) -> 'List a -> 'List b
'Maybe :: Type->Type
Nothing :: {a} -> 'Maybe a
Just :: {a} -> a -> 'Maybe a
'MaybeCase :: {a} -> (c : 'Maybe a -> Type) -> c Nothing -> (e:a -> c (Just e)) -> (g : 'Maybe a) -> c g
match'Maybe :: (b : Type->Type) -> (c:Type -> b ('Maybe c)) -> e:Type -> b e -> b e
'Vector :: 'Nat -> Type->Type
'VectorCase :: {a:'Nat} -> {b} -> (d : 'Vector a b -> Type) -> (e : 'Vector a b) -> d e
match'Vector :: (b : Type->Type) -> (c:'Nat -> d:Type -> b ('Vector c d)) -> f:Type -> b f -> b f
'PrimitiveType :: Type
Triangle :: 'PrimitiveType
Line :: 'PrimitiveType
Point :: 'PrimitiveType
TriangleAdjacency :: 'PrimitiveType
LineAdjacency :: 'PrimitiveType
'PrimitiveTypeCase :: (b : 'PrimitiveType->Type) -> b Triangle -> b Line -> b Point -> b TriangleAdjacency -> b LineAdjacency -> h:'PrimitiveType -> b h
match'PrimitiveType :: (b : Type->Type) -> b 'PrimitiveType -> d:Type -> b d -> b d
'Primitive :: Type -> 'PrimitiveType->Type
PrimPoint :: {a} -> a -> 'Primitive a Point
PrimLine :: {a} -> a -> a -> 'Primitive a Line
PrimTriangle :: {a} -> a -> a -> a -> 'Primitive a Triangle
'PrimitiveCase :: {a} -> (d : b:'PrimitiveType -> 'Primitive a b -> Type) -> (e:a -> d Point (PrimPoint e)) -> (g:a -> h:a -> d Line (PrimLine g h)) -> (j:a -> k:a -> l:a -> d Triangle (PrimTriangle j k l)) -> {n:'PrimitiveType} -> (o : 'Primitive a n) -> d n o
match'Primitive :: (b : Type->Type) -> (c:Type -> d:'PrimitiveType -> b ('Primitive c d)) -> f:Type -> b f -> b f
mapPrimitive :: {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'Primitive a c -> 'Primitive b c
'PrimitiveStream :: 'PrimitiveType -> Type->Type
mapPrimitives :: {a} -> {b} -> {c:'PrimitiveType} -> a->b -> 'List ('Primitive a c) -> 'List ('Primitive b c)
'ListElem :: Type->Type
fetchArrays :: {a:'PrimitiveType} -> {b : 'List Type} -> {c : 'List Type} -> {d : b ~ map Type Type 'ListElem c} -> 'HList c -> 'PrimitiveStream a ('HList b)
fetch :: {a:'PrimitiveType} -> {b} -> 'String -> b -> 'PrimitiveStream a b
'SimpleFragment :: Type->Type
SimpleFragment :: {a} -> 'Vec 3 'Float -> a -> 'SimpleFragment a
'SimpleFragmentCase :: {a} -> (c : 'SimpleFragment a -> Type) -> ((d : 'Vec 3 'Float) -> e:a -> c (SimpleFragment d e)) -> (g : 'SimpleFragment a) -> c g
match'SimpleFragment :: (b : Type->Type) -> (c:Type -> b ('SimpleFragment c)) -> e:Type -> b e -> b e
'Fragment :: 'Nat -> Type->Type
sFragmentValue :: {a} -> 'SimpleFragment a -> a
sFragmentCoords :: {a} -> 'SimpleFragment a -> 'VecS 'Float 3
'FragmentStream :: 'Nat -> Type->Type
customizeDepth :: {a} -> {b:'Nat} -> a->'Float -> 'Fragment b a -> 'Fragment b a
customizeDepths :: {a} -> {b:'Nat} -> a->'Float -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
filterFragment :: {a} -> {b:'Nat} -> a->'Bool -> 'Fragment b a -> 'Fragment b a
filterFragments :: {a} -> {b:'Nat} -> a->'Bool -> 'List ('Vector b ('Maybe ('SimpleFragment a))) -> 'List ('Vector b ('Maybe ('SimpleFragment a)))
mapFragment :: {a} -> {b} -> {c:'Nat} -> a->b -> 'Fragment c a -> 'Fragment c b
mapFragments :: {a} -> {b} -> {c:'Nat} -> a->b -> 'List ('Vector c ('Maybe ('SimpleFragment a))) -> 'List ('Vector c ('Maybe ('SimpleFragment b)))
'ImageSemantics :: Type
Depth :: Type->'ImageSemantics
Stencil :: Type->'ImageSemantics
Color :: Type->'ImageSemantics
'ImageSemanticsCase :: (b : 'ImageSemantics->Type) -> (c:Type -> b (Depth c)) -> (e:Type -> b (Stencil e)) -> (g:Type -> b (Color g)) -> i:'ImageSemantics -> b i
match'ImageSemantics :: (b : Type->Type) -> b 'ImageSemantics -> d:Type -> b d -> b d
'Image :: 'Nat -> 'ImageSemantics->Type
'ImageCase :: {a:'Nat} -> {b:'ImageSemantics} -> (d : 'Image a b -> Type) -> (e : 'Image a b) -> d e
match'Image :: (b : Type->Type) -> (c:'Nat -> d:'ImageSemantics -> b ('Image c d)) -> f:Type -> b f -> b f
ColorImage :: {a:'Nat} -> {b:'Nat} -> {c} -> {d} -> {e : 'Num c} -> {f : d ~ 'VecScalar b c} -> d -> 'Image a (Color d)
DepthImage :: {a:'Nat} -> 'Float -> 'Image a (Depth 'Float)
StencilImage :: {a:'Nat} -> 'Int -> 'Image a (Stencil 'Int)
emptyDepthImage :: 'Float -> 'Image 1 (Depth 'Float)
emptyColorImage :: {a:'Nat} -> {b} -> {c} -> {d : 'Num b} -> {e : c ~ 'VecScalar a b} -> c -> 'Image 1 (Color c)
'Swizz :: Type
Sx :: 'Swizz
Sy :: 'Swizz
Sz :: 'Swizz
Sw :: 'Swizz
'SwizzCase :: (b : 'Swizz->Type) -> b Sx -> b Sy -> b Sz -> b Sw -> g:'Swizz -> b g
match'Swizz :: (b : Type->Type) -> b 'Swizz -> d:Type -> b d -> b d
swizzscalar :: {a} -> {b:'Nat} -> 'Vec b a -> 'Swizz->a
definedVec :: {a} -> {b:'Nat} -> 'Vec b a -> 'Bool
swizzvector :: {a} -> {b:'Nat} -> {c:'Nat} -> 'Vec b a -> 'Vec c 'Swizz -> 'VecS a c
'BlendingFactor :: Type
Zero' :: 'BlendingFactor
One :: 'BlendingFactor
SrcColor :: 'BlendingFactor
OneMinusSrcColor :: 'BlendingFactor
DstColor :: 'BlendingFactor
OneMinusDstColor :: 'BlendingFactor
SrcAlpha :: 'BlendingFactor
OneMinusSrcAlpha :: 'BlendingFactor
DstAlpha :: 'BlendingFactor
OneMinusDstAlpha :: 'BlendingFactor
ConstantColor :: 'BlendingFactor
OneMinusConstantColor :: 'BlendingFactor
ConstantAlpha :: 'BlendingFactor
OneMinusConstantAlpha :: 'BlendingFactor
SrcAlphaSaturate :: 'BlendingFactor
'BlendingFactorCase :: (b : 'BlendingFactor->Type) -> b Zero' -> b One -> b SrcColor -> b OneMinusSrcColor -> b DstColor -> b OneMinusDstColor -> b SrcAlpha -> b OneMinusSrcAlpha -> b DstAlpha -> b OneMinusDstAlpha -> b ConstantColor -> b OneMinusConstantColor -> b ConstantAlpha -> b OneMinusConstantAlpha -> b SrcAlphaSaturate -> r:'BlendingFactor -> b r
match'BlendingFactor :: (b : Type->Type) -> b 'BlendingFactor -> d:Type -> b d -> b d
'BlendEquation :: Type
FuncAdd :: 'BlendEquation
FuncSubtract :: 'BlendEquation
FuncReverseSubtract :: 'BlendEquation
Min :: 'BlendEquation
Max :: 'BlendEquation
'BlendEquationCase :: (b : 'BlendEquation->Type) -> b FuncAdd -> b FuncSubtract -> b FuncReverseSubtract -> b Min -> b Max -> h:'BlendEquation -> b h
match'BlendEquation :: (b : Type->Type) -> b 'BlendEquation -> d:Type -> b d -> b d
'LogicOperation :: Type
Clear :: 'LogicOperation
And :: 'LogicOperation
AndReverse :: 'LogicOperation
Copy :: 'LogicOperation
AndInverted :: 'LogicOperation
Noop :: 'LogicOperation
Xor :: 'LogicOperation
Or :: 'LogicOperation
Nor :: 'LogicOperation
Equiv :: 'LogicOperation
Invert :: 'LogicOperation
OrReverse :: 'LogicOperation
CopyInverted :: 'LogicOperation
OrInverted :: 'LogicOperation
Nand :: 'LogicOperation
Set :: 'LogicOperation
'LogicOperationCase :: (b : 'LogicOperation->Type) -> b Clear -> b And -> b AndReverse -> b Copy -> b AndInverted -> b Noop -> b Xor -> b Or -> b Nor -> b Equiv -> b Invert -> b OrReverse -> b CopyInverted -> b OrInverted -> b Nand -> b Set -> s:'LogicOperation -> b s
match'LogicOperation :: (b : Type->Type) -> b 'LogicOperation -> d:Type -> b d -> b d
'StencilOperation :: Type
OpZero :: 'StencilOperation
OpKeep :: 'StencilOperation
OpReplace :: 'StencilOperation
OpIncr :: 'StencilOperation
OpIncrWrap :: 'StencilOperation
OpDecr :: 'StencilOperation
OpDecrWrap :: 'StencilOperation
OpInvert :: 'StencilOperation
'StencilOperationCase :: (b : 'StencilOperation->Type) -> b OpZero -> b OpKeep -> b OpReplace -> b OpIncr -> b OpIncrWrap -> b OpDecr -> b OpDecrWrap -> b OpInvert -> k:'StencilOperation -> b k
match'StencilOperation :: (b : Type->Type) -> b 'StencilOperation -> d:Type -> b d -> b d
'ComparisonFunction :: Type
Never :: 'ComparisonFunction
Less :: 'ComparisonFunction
Equal :: 'ComparisonFunction
Lequal :: 'ComparisonFunction
Greater :: 'ComparisonFunction
Notequal :: 'ComparisonFunction
Gequal :: 'ComparisonFunction
Always :: 'ComparisonFunction
'ComparisonFunctionCase :: (b : 'ComparisonFunction->Type) -> b Never -> b Less -> b Equal -> b Lequal -> b Greater -> b Notequal -> b Gequal -> b Always -> k:'ComparisonFunction -> b k
match'ComparisonFunction :: (b : Type->Type) -> b 'ComparisonFunction -> d:Type -> b d -> b d
'ProvokingVertex :: Type
LastVertex :: 'ProvokingVertex
FirstVertex :: 'ProvokingVertex
'ProvokingVertexCase :: (b : 'ProvokingVertex->Type) -> b LastVertex -> b FirstVertex -> e:'ProvokingVertex -> b e
match'ProvokingVertex :: (b : Type->Type) -> b 'ProvokingVertex -> d:Type -> b d -> b d
'CullMode :: Type
CullFront :: 'CullMode
CullBack :: 'CullMode
CullNone :: 'CullMode
'CullModeCase :: (b : 'CullMode->Type) -> b CullFront -> b CullBack -> b CullNone -> f:'CullMode -> b f
match'CullMode :: (b : Type->Type) -> b 'CullMode -> d:Type -> b d -> b d
'PointSize :: Type->Type
PointSize :: {a} -> 'Float -> 'PointSize a
ProgramPointSize :: {a} -> a->'Float -> 'PointSize a
'PointSizeCase :: {a} -> (c : 'PointSize a -> Type) -> (d:'Float -> c (PointSize d)) -> ((g : a->'Float) -> c (ProgramPointSize g)) -> (i : 'PointSize a) -> c i
match'PointSize :: (b : Type->Type) -> (c:Type -> b ('PointSize c)) -> e:Type -> b e -> b e
'PolygonMode :: Type->Type
PolygonFill :: {a} -> 'PolygonMode a
PolygonPoint :: {a} -> 'PointSize a -> 'PolygonMode a
PolygonLine :: {a} -> 'Float -> 'PolygonMode a
'PolygonModeCase :: {a} -> (c : 'PolygonMode a -> Type) -> c PolygonFill -> ((e : 'PointSize a) -> c (PolygonPoint e)) -> (g:'Float -> c (PolygonLine g)) -> (i : 'PolygonMode a) -> c i
match'PolygonMode :: (b : Type->Type) -> (c:Type -> b ('PolygonMode c)) -> e:Type -> b e -> b e
'PolygonOffset :: Type
NoOffset :: 'PolygonOffset
Offset :: 'Float -> 'Float->'PolygonOffset
'PolygonOffsetCase :: (b : 'PolygonOffset->Type) -> b NoOffset -> (d:'Float -> e:'Float -> b (Offset d e)) -> g:'PolygonOffset -> b g
match'PolygonOffset :: (b : Type->Type) -> b 'PolygonOffset -> d:Type -> b d -> b d
'PointSpriteCoordOrigin :: Type
LowerLeft :: 'PointSpriteCoordOrigin
UpperLeft :: 'PointSpriteCoordOrigin
'PointSpriteCoordOriginCase :: (b : 'PointSpriteCoordOrigin->Type) -> b LowerLeft -> b UpperLeft -> e:'PointSpriteCoordOrigin -> b e
match'PointSpriteCoordOrigin :: (b : Type->Type) -> b 'PointSpriteCoordOrigin -> d:Type -> b d -> b d
primTexture :: () -> 'Vec 2 'Float -> 'Vec 4 'Float
Uniform :: {a} -> 'String->a
Attribute :: {a} -> 'String->a
'RasterContext :: Type -> 'PrimitiveType->Type
TriangleCtx :: {a} -> 'CullMode -> 'PolygonMode a -> 'PolygonOffset -> 'ProvokingVertex -> 'RasterContext a Triangle
PointCtx :: {a} -> 'PointSize a -> 'Float -> 'PointSpriteCoordOrigin -> 'RasterContext a Point
LineCtx :: {a} -> 'Float -> 'ProvokingVertex -> 'RasterContext a Line
'RasterContextCase :: {a} -> (d : b:'PrimitiveType -> 'RasterContext a b -> Type) -> (e:'CullMode -> (f : 'PolygonMode a) -> g:'PolygonOffset -> h:'ProvokingVertex -> d Triangle (TriangleCtx e f g h)) -> ((j : 'PointSize a) -> k:'Float -> l:'PointSpriteCoordOrigin -> d Point (PointCtx j k l)) -> (n:'Float -> o:'ProvokingVertex -> d Line (LineCtx n o)) -> {q:'PrimitiveType} -> (r : 'RasterContext a q) -> d q r
match'RasterContext :: (b : Type->Type) -> (c:Type -> d:'PrimitiveType -> b ('RasterContext c d)) -> f:Type -> b f -> b f
'Blending :: Type->Type
NoBlending :: {a} -> 'Blending a
BlendLogicOp :: {a} -> {b : 'Integral a} -> 'LogicOperation -> 'Blending a
Blend :: ('BlendEquation, 'BlendEquation) -> (('BlendingFactor, 'BlendingFactor), ('BlendingFactor, 'BlendingFactor)) -> 'Vec 4 'Float -> 'Blending 'Float
'BlendingCase :: (c : a:Type -> 'Blending a -> Type) -> ({d} -> c d (NoBlending d)) -> ({f} -> {g : 'Integral f} -> h:'LogicOperation -> c f (BlendLogicOp f g h)) -> (j:('BlendEquation, 'BlendEquation) -> k:(('BlendingFactor, 'BlendingFactor), ('BlendingFactor, 'BlendingFactor)) -> (l : 'Vec 4 'Float) -> c 'Float (Blend j k l)) -> {n} -> (o : 'Blending n) -> c n o
match'Blending :: (b : Type->Type) -> (c:Type -> b ('Blending c)) -> e:Type -> b e -> b e
'StencilTests :: Type
'StencilTestsCase :: (b : 'StencilTests->Type) -> c:'StencilTests -> b c
match'StencilTests :: (b : Type->Type) -> b 'StencilTests -> d:Type -> b d -> b d
'StencilOps :: Type
'StencilOpsCase :: (b : 'StencilOps->Type) -> c:'StencilOps -> b c
match'StencilOps :: (b : Type->Type) -> b 'StencilOps -> d:Type -> b d -> b d
'Int32 :: Type
'Int32Case :: (b : 'Int32->Type) -> c:'Int32 -> b c
match'Int32 :: (b : Type->Type) -> b 'Int32 -> d:Type -> b d -> b d
'FragmentOperation :: 'ImageSemantics->Type
ColorOp :: {a} -> {b:'Nat} -> {c : 'Num a} -> 'Blending a -> 'VecScalar b 'Bool -> 'FragmentOperation (Color ('VecScalar b a))
DepthOp :: 'ComparisonFunction -> 'Bool -> 'FragmentOperation (Depth 'Float)
StencilOp :: 'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation (Stencil 'Int32)
'FragmentOperationCase :: (c : a:'ImageSemantics -> 'FragmentOperation a -> Type) -> ({d} -> {e:'Nat} -> {f : 'Num d} -> (g : 'Blending d) -> (h : 'VecScalar e 'Bool) -> c (Color ('VecScalar e d)) (ColorOp d e f g h)) -> (j:'ComparisonFunction -> k:'Bool -> c (Depth 'Float) (DepthOp j k)) -> (m:'StencilTests -> n:'StencilOps -> o:'StencilOps -> c (Stencil 'Int32) (StencilOp m n o)) -> {q:'ImageSemantics} -> (r : 'FragmentOperation q) -> c q r
match'FragmentOperation :: (b : Type->Type) -> (c:'ImageSemantics -> b ('FragmentOperation c)) -> e:Type -> b e -> b e
'Interpolated :: Type->Type
Smooth :: {a} -> {b : 'Floating a} -> 'Interpolated a
NoPerspective :: {a} -> {b : 'Floating a} -> 'Interpolated a
Flat :: {a} -> 'Interpolated a
'InterpolatedCase :: {a} -> (c : 'Interpolated a -> Type) -> ({d : 'Floating a} -> c (Smooth d)) -> ({f : 'Floating a} -> c (NoPerspective f)) -> c Flat -> (i : 'Interpolated a) -> c i
match'Interpolated :: (b : Type->Type) -> (c:Type -> b ('Interpolated c)) -> e:Type -> b e -> b e
rasterizePrimitive :: {a : 'List Type} -> {b : 'List Type} -> {c : 'List Type} -> {d:'PrimitiveType} -> {e : map Type Type 'Interpolated a ~ b} -> {f : c ~ Cons ('Vec 4 'Float) a} -> 'HList b -> 'RasterContext ('HList c) d -> 'Primitive ('HList c) d -> 'FragmentStream 1 ('HList a)
rasterizePrimitives :: {a : 'List Type} -> {b:'PrimitiveType} -> 'RasterContext ('HList (Cons ('Vec 4 'Float) a)) b -> 'HList (map Type Type 'Interpolated a) -> 'List ('Primitive ('HList (Cons ('Vec 4 'Float) a)) b) -> 'List ('Vector 1 ('Maybe ('SimpleFragment ('HList a))))
'ImageLC :: Type->'Nat
allSame :: {a} -> 'List a -> Type
sameLayerCounts :: 'List Type -> Type
'FrameBuffer :: 'Nat -> 'List 'ImageSemantics -> Type
'FrameBufferCase :: {a:'Nat} -> {b : 'List 'ImageSemantics} -> (d : 'FrameBuffer a b -> Type) -> (e : 'FrameBuffer a b) -> d e
match'FrameBuffer :: (b : Type->Type) -> (c:'Nat -> (d : 'List 'ImageSemantics) -> b ('FrameBuffer c d)) -> f:Type -> b f -> b f
remSemantics :: 'ImageSemantics->Type
remSemantics' :: 'List 'ImageSemantics -> 'List Type
'FragmentOperationSem :: Type->'ImageSemantics
Accumulate :: {a : 'List 'ImageSemantics} -> {b:'Nat} -> {c : 'List Type} -> {d : a ~ map Type 'ImageSemantics 'FragmentOperationSem c} -> 'HList c -> 'FragmentStream b ('HList (remSemantics' a)) -> 'FrameBuffer b a -> 'FrameBuffer b a
accumulateWith :: {a} -> {b} -> a -> b->(a, b)
overlay :: {a:'Nat} -> {b : 'List Type} -> 'FrameBuffer a (map Type 'ImageSemantics 'FragmentOperationSem b) -> ('HList b, 'List ('Fragment a ('HList (remSemantics' (map Type 'ImageSemantics 'FragmentOperationSem b))))) -> 'FrameBuffer a (map Type 'ImageSemantics 'FragmentOperationSem b)
'ImageSem :: Type->'ImageSemantics
FrameBuffer :: {a : 'List Type} -> {b : sameLayerCounts a} -> 'HList a -> 'FrameBuffer ('ImageLC (head Type a)) (map Type 'ImageSemantics 'ImageSem a)
imageFrame :: {a : 'List Type} -> {b : sameLayerCounts a} -> 'HList a -> 'FrameBuffer ('ImageLC (head Type a)) (map Type 'ImageSemantics 'ImageSem a)
accumulate :: {a:'Nat} -> {b : 'List Type} -> {c} -> 'HList b -> (c -> 'HList (remSemantics' (map Type 'ImageSemantics 'FragmentOperationSem b))) -> 'List ('Vector a ('Maybe ('SimpleFragment c))) -> 'FrameBuffer a (map Type 'ImageSemantics 'FragmentOperationSem b) -> 'FrameBuffer a (map Type 'ImageSemantics 'FragmentOperationSem b)
PrjImage :: {a:'ImageSemantics} -> 'FrameBuffer 1 (Cons a Nil) -> 'Image 1 a
PrjImageColor :: 'FrameBuffer 1 (Cons (Depth 'Float) (Cons (Color ('Vec 4 'Float)) Nil)) -> 'Image 1 (Color ('Vec 4 'Float))
'Output :: Type
ScreenOut :: {a:'Nat} -> {b : 'List 'ImageSemantics} -> 'FrameBuffer a b -> 'Output
'OutputCase :: (b : 'Output->Type) -> ({c:'Nat} -> {d : 'List 'ImageSemantics} -> (e : 'FrameBuffer c d) -> b (ScreenOut c d e)) -> g:'Output -> b g
match'Output :: (b : Type->Type) -> b 'Output -> d:Type -> b d -> b d
renderFrame :: {a:'Nat} -> {b : 'List 'ImageSemantics} -> 'FrameBuffer a b -> 'Output
'Texture :: Type
Texture2DSlot :: 'String->'Texture
Texture2D :: 'Vec 2 'Int -> 'Image 1 (Color ('Vec 4 'Float)) -> 'Texture
'TextureCase :: (b : 'Texture->Type) -> (c:'String -> b (Texture2DSlot c)) -> ((e : 'Vec 2 'Int) -> (f : 'Image 1 (Color ('Vec 4 'Float))) -> b (Texture2D e f)) -> h:'Texture -> b h
match'Texture :: (b : Type->Type) -> b 'Texture -> d:Type -> b d -> b d
'Filter :: Type
PointFilter :: 'Filter
LinearFilter :: 'Filter
'FilterCase :: (b : 'Filter->Type) -> b PointFilter -> b LinearFilter -> e:'Filter -> b e
match'Filter :: (b : Type->Type) -> b 'Filter -> d:Type -> b d -> b d
'EdgeMode :: Type
Repeat :: 'EdgeMode
MirroredRepeat :: 'EdgeMode
ClampToEdge :: 'EdgeMode
'EdgeModeCase :: (b : 'EdgeMode->Type) -> b Repeat -> b MirroredRepeat -> b ClampToEdge -> f:'EdgeMode -> b f
match'EdgeMode :: (b : Type->Type) -> b 'EdgeMode -> d:Type -> b d -> b d
'Sampler :: Type
Sampler :: 'Filter -> 'EdgeMode -> 'Texture->'Sampler
'SamplerCase :: (b : 'Sampler->Type) -> (c:'Filter -> d:'EdgeMode -> e:'Texture -> b (Sampler c d e)) -> g:'Sampler -> b g
match'Sampler :: (b : Type->Type) -> b 'Sampler -> d:Type -> b d -> b d
texture2D :: 'Sampler -> 'Vec 2 'Float -> 'Vec 4 'Float
accumulationContext :: {a} -> a->a
------------ tooltips
testdata/Builtins.lc 10:1-10:3  {a} -> a->a
testdata/Builtins.lc 10:8-10:9  V1
testdata/Builtins.lc 14:6-14:10  Type | Type -> Nat->Type
testdata/Builtins.lc 14:6-17:37  Type
testdata/Builtins.lc 14:17-14:21  Type
testdata/Builtins.lc 14:26-14:29  Type
testdata/Builtins.lc 14:26-14:37  Type
testdata/Builtins.lc 14:33-14:37  Type
testdata/Builtins.lc 15:3-15:5  VecS V3 2 | {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 15:3-15:27  Type
testdata/Builtins.lc 15:9-15:10  Type
testdata/Builtins.lc 15:9-15:27  Type
testdata/Builtins.lc 15:14-15:15  Type
testdata/Builtins.lc 15:14-15:27  Type
testdata/Builtins.lc 15:19-15:23  Type -> Nat->Type
testdata/Builtins.lc 15:19-15:25  Nat->Type
testdata/Builtins.lc 15:19-15:27  Type
testdata/Builtins.lc 15:24-15:25  Type
testdata/Builtins.lc 15:26-15:27  V1
testdata/Builtins.lc 16:3-16:5  VecS V5 3 | {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 16:3-16:32  Type
testdata/Builtins.lc 16:9-16:10  Type
testdata/Builtins.lc 16:9-16:32  Type
testdata/Builtins.lc 16:14-16:15  Type
testdata/Builtins.lc 16:14-16:32  Type
testdata/Builtins.lc 16:19-16:20  Type
testdata/Builtins.lc 16:19-16:32  Type
testdata/Builtins.lc 16:24-16:28  Type -> Nat->Type
testdata/Builtins.lc 16:24-16:30  Nat->Type
testdata/Builtins.lc 16:24-16:32  Type
testdata/Builtins.lc 16:29-16:30  Type
testdata/Builtins.lc 16:31-16:32  V1
testdata/Builtins.lc 17:3-17:5  VecS V7 4 | {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 17:3-17:37  Type
testdata/Builtins.lc 17:9-17:10  Type
testdata/Builtins.lc 17:9-17:37  Type
testdata/Builtins.lc 17:14-17:15  Type
testdata/Builtins.lc 17:14-17:37  Type
testdata/Builtins.lc 17:19-17:20  Type
testdata/Builtins.lc 17:19-17:37  Type
testdata/Builtins.lc 17:24-17:25  Type
testdata/Builtins.lc 17:24-17:37  Type
testdata/Builtins.lc 17:29-17:33  Type -> Nat->Type
testdata/Builtins.lc 17:29-17:35  Nat->Type
testdata/Builtins.lc 17:29-17:37  Type
testdata/Builtins.lc 17:34-17:35  Type
testdata/Builtins.lc 17:36-17:37  V1
testdata/Builtins.lc 19:11-19:43  Type
testdata/Builtins.lc 19:12-19:13  V5
testdata/Builtins.lc 19:17-19:18  Type | V4
testdata/Builtins.lc 19:23-19:27  Type -> Nat->Type
testdata/Builtins.lc 19:23-19:29  Nat->Type
testdata/Builtins.lc 19:23-19:31  Type
testdata/Builtins.lc 19:23-19:43  Type
testdata/Builtins.lc 19:28-19:29  Type
testdata/Builtins.lc 19:30-19:31  V2
testdata/Builtins.lc 19:35-19:39  Type -> Nat->Type
testdata/Builtins.lc 19:35-19:41  Nat->Type
testdata/Builtins.lc 19:35-19:43  Type
testdata/Builtins.lc 19:40-19:41  Type
testdata/Builtins.lc 19:42-19:43  Nat
testdata/Builtins.lc 20:1-20:7  {a} -> {b} -> {c:Nat} -> a->b -> VecS a c -> VecS b c
testdata/Builtins.lc 20:11-20:13  VecS V5 V3
testdata/Builtins.lc 20:11-22:51  V2->V2 -> VecS V3 V1 -> VecS V3 V2 | VecS V3 V1 -> VecS V3 V2 | VecS V3 V2
testdata/Builtins.lc 20:21-20:23  {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 20:21-20:29  V5 -> VecS V6 2
testdata/Builtins.lc 20:21-20:35  V0 -> V1 -> VecS V6 2 | V1 -> VecS V6 2 | VecS V5 2
testdata/Builtins.lc 20:21-21:43  (V4 -> V5 -> V6 -> V7 -> VecS V7 4) -> {f:Nat} -> VecS V6 f -> VecS V6 f
testdata/Builtins.lc 20:21-22:51  {a:Nat} -> VecS V5 a -> VecS V5 a
testdata/Builtins.lc 20:25-20:26  V8->V8
testdata/Builtins.lc 20:25-20:28  V5
testdata/Builtins.lc 20:27-20:28  V2
testdata/Builtins.lc 20:31-20:32  V6->V6
testdata/Builtins.lc 20:31-20:34  V5
testdata/Builtins.lc 20:33-20:34  V6
testdata/Builtins.lc 21:23-21:25  {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 21:23-21:31  V6 -> V7 -> VecS V8 3
testdata/Builtins.lc 21:23-21:37  V6 -> VecS V7 3
testdata/Builtins.lc 21:23-21:43  V4 -> V5 -> V6 -> VecS V6 3 | V5 -> V6 -> VecS V6 3 | V6 -> VecS V6 3 | VecS V6 3
testdata/Builtins.lc 21:27-21:28  V8->V8
testdata/Builtins.lc 21:27-21:30  V6
testdata/Builtins.lc 21:29-21:30  V7
testdata/Builtins.lc 21:33-21:34  V7->V7
testdata/Builtins.lc 21:33-21:36  V6
testdata/Builtins.lc 21:35-21:36  V7
testdata/Builtins.lc 21:39-21:40  V7->V7
testdata/Builtins.lc 21:39-21:42  V6
testdata/Builtins.lc 21:41-21:42  V7
testdata/Builtins.lc 22:25-22:27  {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 22:25-22:33  V7 -> V8 -> V9 -> VecS V10 4
testdata/Builtins.lc 22:25-22:39  V7 -> V8 -> VecS V9 4
testdata/Builtins.lc 22:25-22:45  V7 -> VecS V8 4
testdata/Builtins.lc 22:25-22:51  V4 -> V5 -> V6 -> V7 -> VecS V7 4 | V5 -> V6 -> V7 -> VecS V7 4 | V6 -> V7 -> VecS V7 4 | V7 -> VecS V7 4 | VecS V7 4
testdata/Builtins.lc 22:29-22:30  V9->V9
testdata/Builtins.lc 22:29-22:32  V7
testdata/Builtins.lc 22:31-22:32  V8
testdata/Builtins.lc 22:35-22:36  V8->V8
testdata/Builtins.lc 22:35-22:38  V7
testdata/Builtins.lc 22:37-22:38  V8
testdata/Builtins.lc 22:41-22:42  V8->V8
testdata/Builtins.lc 22:41-22:44  V7
testdata/Builtins.lc 22:43-22:44  V8
testdata/Builtins.lc 22:47-22:48  V8->V8
testdata/Builtins.lc 22:47-22:50  V7
testdata/Builtins.lc 22:49-22:50  V8
testdata/Builtins.lc 24:23-24:26  Type
testdata/Builtins.lc 24:37-24:40  Nat -> Type->Type
testdata/Builtins.lc 24:47-24:51  Type -> Nat->Type
testdata/Builtins.lc 24:47-24:53  Nat->Type
testdata/Builtins.lc 24:47-24:55  Nat -> Type->Type | Type | Type->Type
testdata/Builtins.lc 24:52-24:53  Type
testdata/Builtins.lc 24:54-24:55  Nat
testdata/Builtins.lc 27:29-27:32  Type
testdata/Builtins.lc 28:5-28:14  Nat -> Type->Type
testdata/Builtins.lc 28:21-28:22  Type
testdata/Builtins.lc 28:21-29:60  Nat -> Type->Type | Nat->Type | Type->Type
testdata/Builtins.lc 29:37-29:40  Nat -> Type->Type
testdata/Builtins.lc 29:37-29:58  Type->Type
testdata/Builtins.lc 29:37-29:60  Nat->Type | Type
testdata/Builtins.lc 29:42-29:47  Nat->Nat
testdata/Builtins.lc 29:42-29:57  Nat
testdata/Builtins.lc 29:49-29:54  Nat->Nat
testdata/Builtins.lc 29:49-29:56  Nat
testdata/Builtins.lc 29:55-29:56  Nat
testdata/Builtins.lc 29:59-29:60  Type
testdata/Builtins.lc 32:6-32:9  Nat -> Nat -> Type->Type | Type
testdata/Builtins.lc 32:6-41:84  Type
testdata/Builtins.lc 32:13-32:16  Type
testdata/Builtins.lc 32:20-32:23  Type
testdata/Builtins.lc 32:20-32:39  Type
testdata/Builtins.lc 32:27-32:31  Type
testdata/Builtins.lc 32:27-32:39  Type
testdata/Builtins.lc 32:35-32:39  Type
testdata/Builtins.lc 33:3-33:7  Mat 2 2 Float | Vec 2 Float -> Vec 2 Float -> Mat 2 2 Float
testdata/Builtins.lc 33:3-33:54  Type
testdata/Builtins.lc 33:11-33:14  Nat -> Type->Type
testdata/Builtins.lc 33:11-33:16  Type->Type
testdata/Builtins.lc 33:11-33:22  Type
testdata/Builtins.lc 33:15-33:16  V1
testdata/Builtins.lc 33:17-33:22  Type
testdata/Builtins.lc 33:26-33:29  Nat -> Type->Type
testdata/Builtins.lc 33:26-33:31  Type->Type
testdata/Builtins.lc 33:26-33:37  Type
testdata/Builtins.lc 33:26-33:54  Type
testdata/Builtins.lc 33:30-33:31  V1
testdata/Builtins.lc 33:32-33:37  Type
testdata/Builtins.lc 33:41-33:44  Nat -> Nat -> Type->Type
testdata/Builtins.lc 33:41-33:46  Nat -> Type->Type
testdata/Builtins.lc 33:41-33:48  Type->Type
testdata/Builtins.lc 33:41-33:54  Type
testdata/Builtins.lc 33:45-33:46  V1
testdata/Builtins.lc 33:45-33:48  a:Type -> Mat 2 2 a -> Type
testdata/Builtins.lc 33:45-33:54  Mat 2 2 Float -> Type
testdata/Builtins.lc 33:47-33:48  V1
testdata/Builtins.lc 33:49-33:54  Type
testdata/Builtins.lc 34:3-34:7  Mat 3 2 Float | Vec 3 Float -> Vec 3 Float -> Mat 3 2 Float
testdata/Builtins.lc 34:3-34:54  Type
testdata/Builtins.lc 34:11-34:14  Nat -> Type->Type
testdata/Builtins.lc 34:11-34:16  Type->Type
testdata/Builtins.lc 34:11-34:22  Type
testdata/Builtins.lc 34:15-34:16  V1
testdata/Builtins.lc 34:17-34:22  Type
testdata/Builtins.lc 34:26-34:29  Nat -> Type->Type
testdata/Builtins.lc 34:26-34:31  Type->Type
testdata/Builtins.lc 34:26-34:37  Type
testdata/Builtins.lc 34:26-34:54  Type
testdata/Builtins.lc 34:30-34:31  V1
testdata/Builtins.lc 34:32-34:37  Type
testdata/Builtins.lc 34:41-34:44  Nat -> Nat -> Type->Type
testdata/Builtins.lc 34:41-34:46  Nat -> Type->Type
testdata/Builtins.lc 34:41-34:48  Type->Type
testdata/Builtins.lc 34:41-34:54  Type
testdata/Builtins.lc 34:45-34:46  V1
testdata/Builtins.lc 34:45-34:48  a:Type -> Mat 3 2 a -> Type
testdata/Builtins.lc 34:45-34:54  Mat 3 2 Float -> Type
testdata/Builtins.lc 34:47-34:48  V1
testdata/Builtins.lc 34:49-34:54  Type
testdata/Builtins.lc 35:3-35:7  Mat 4 2 Float | Vec 4 Float -> Vec 4 Float -> Mat 4 2 Float
testdata/Builtins.lc 35:3-35:54  Type
testdata/Builtins.lc 35:11-35:14  Nat -> Type->Type
testdata/Builtins.lc 35:11-35:16  Type->Type
testdata/Builtins.lc 35:11-35:22  Type
testdata/Builtins.lc 35:15-35:16  V1
testdata/Builtins.lc 35:17-35:22  Type
testdata/Builtins.lc 35:26-35:29  Nat -> Type->Type
testdata/Builtins.lc 35:26-35:31  Type->Type
testdata/Builtins.lc 35:26-35:37  Type
testdata/Builtins.lc 35:26-35:54  Type
testdata/Builtins.lc 35:30-35:31  V1
testdata/Builtins.lc 35:32-35:37  Type
testdata/Builtins.lc 35:41-35:44  Nat -> Nat -> Type->Type
testdata/Builtins.lc 35:41-35:46  Nat -> Type->Type
testdata/Builtins.lc 35:41-35:48  Type->Type
testdata/Builtins.lc 35:41-35:54  Type
testdata/Builtins.lc 35:45-35:46  V1
testdata/Builtins.lc 35:45-35:48  a:Type -> Mat 4 2 a -> Type
testdata/Builtins.lc 35:45-35:54  Mat 4 2 Float -> Type
testdata/Builtins.lc 35:47-35:48  V1
testdata/Builtins.lc 35:49-35:54  Type
testdata/Builtins.lc 36:3-36:7  Mat 2 3 Float | Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 3 Float
testdata/Builtins.lc 36:3-36:69  Type
testdata/Builtins.lc 36:11-36:14  Nat -> Type->Type
testdata/Builtins.lc 36:11-36:16  Type->Type
testdata/Builtins.lc 36:11-36:22  Type
testdata/Builtins.lc 36:15-36:16  V1
testdata/Builtins.lc 36:17-36:22  Type
testdata/Builtins.lc 36:26-36:29  Nat -> Type->Type
testdata/Builtins.lc 36:26-36:31  Type->Type
testdata/Builtins.lc 36:26-36:37  Type
testdata/Builtins.lc 36:26-36:69  Type
testdata/Builtins.lc 36:30-36:31  V1
testdata/Builtins.lc 36:32-36:37  Type
testdata/Builtins.lc 36:41-36:44  Nat -> Type->Type
testdata/Builtins.lc 36:41-36:46  Type->Type
testdata/Builtins.lc 36:41-36:52  Type
testdata/Builtins.lc 36:41-36:69  Type
testdata/Builtins.lc 36:45-36:46  V1
testdata/Builtins.lc 36:47-36:52  Type
testdata/Builtins.lc 36:56-36:59  Nat -> Nat -> Type->Type
testdata/Builtins.lc 36:56-36:61  Nat -> Type->Type
testdata/Builtins.lc 36:56-36:63  Type->Type
testdata/Builtins.lc 36:56-36:69  Type
testdata/Builtins.lc 36:60-36:61  V1
testdata/Builtins.lc 36:60-36:63  a:Type -> Mat 2 3 a -> Type
testdata/Builtins.lc 36:60-36:69  Mat 2 3 Float -> Type
testdata/Builtins.lc 36:62-36:63  V1
testdata/Builtins.lc 36:64-36:69  Type
testdata/Builtins.lc 37:3-37:7  Mat 3 3 Float | Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 3 Float
testdata/Builtins.lc 37:3-37:69  Type
testdata/Builtins.lc 37:11-37:14  Nat -> Type->Type
testdata/Builtins.lc 37:11-37:16  Type->Type
testdata/Builtins.lc 37:11-37:22  Type
testdata/Builtins.lc 37:15-37:16  V1
testdata/Builtins.lc 37:17-37:22  Type
testdata/Builtins.lc 37:26-37:29  Nat -> Type->Type
testdata/Builtins.lc 37:26-37:31  Type->Type
testdata/Builtins.lc 37:26-37:37  Type
testdata/Builtins.lc 37:26-37:69  Type
testdata/Builtins.lc 37:30-37:31  V1
testdata/Builtins.lc 37:32-37:37  Type
testdata/Builtins.lc 37:41-37:44  Nat -> Type->Type
testdata/Builtins.lc 37:41-37:46  Type->Type
testdata/Builtins.lc 37:41-37:52  Type
testdata/Builtins.lc 37:41-37:69  Type
testdata/Builtins.lc 37:45-37:46  V1
testdata/Builtins.lc 37:47-37:52  Type
testdata/Builtins.lc 37:56-37:59  Nat -> Nat -> Type->Type
testdata/Builtins.lc 37:56-37:61  Nat -> Type->Type
testdata/Builtins.lc 37:56-37:63  Type->Type
testdata/Builtins.lc 37:56-37:69  Type
testdata/Builtins.lc 37:60-37:61  V1
testdata/Builtins.lc 37:60-37:63  a:Type -> Mat 3 3 a -> Type
testdata/Builtins.lc 37:60-37:69  Mat 3 3 Float -> Type
testdata/Builtins.lc 37:62-37:63  V1
testdata/Builtins.lc 37:64-37:69  Type
testdata/Builtins.lc 38:3-38:7  Mat 4 3 Float | Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 3 Float
testdata/Builtins.lc 38:3-38:69  Type
testdata/Builtins.lc 38:11-38:14  Nat -> Type->Type
testdata/Builtins.lc 38:11-38:16  Type->Type
testdata/Builtins.lc 38:11-38:22  Type
testdata/Builtins.lc 38:15-38:16  V1
testdata/Builtins.lc 38:17-38:22  Type
testdata/Builtins.lc 38:26-38:29  Nat -> Type->Type
testdata/Builtins.lc 38:26-38:31  Type->Type
testdata/Builtins.lc 38:26-38:37  Type
testdata/Builtins.lc 38:26-38:69  Type
testdata/Builtins.lc 38:30-38:31  V1
testdata/Builtins.lc 38:32-38:37  Type
testdata/Builtins.lc 38:41-38:44  Nat -> Type->Type
testdata/Builtins.lc 38:41-38:46  Type->Type
testdata/Builtins.lc 38:41-38:52  Type
testdata/Builtins.lc 38:41-38:69  Type
testdata/Builtins.lc 38:45-38:46  V1
testdata/Builtins.lc 38:47-38:52  Type
testdata/Builtins.lc 38:56-38:59  Nat -> Nat -> Type->Type
testdata/Builtins.lc 38:56-38:61  Nat -> Type->Type
testdata/Builtins.lc 38:56-38:63  Type->Type
testdata/Builtins.lc 38:56-38:69  Type
testdata/Builtins.lc 38:60-38:61  V1
testdata/Builtins.lc 38:60-38:63  a:Type -> Mat 4 3 a -> Type
testdata/Builtins.lc 38:60-38:69  Mat 4 3 Float -> Type
testdata/Builtins.lc 38:62-38:63  V1
testdata/Builtins.lc 38:64-38:69  Type
testdata/Builtins.lc 39:3-39:7  Mat 2 4 Float | Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Vec 2 Float -> Mat 2 4 Float
testdata/Builtins.lc 39:3-39:84  Type
testdata/Builtins.lc 39:11-39:14  Nat -> Type->Type
testdata/Builtins.lc 39:11-39:16  Type->Type
testdata/Builtins.lc 39:11-39:22  Type
testdata/Builtins.lc 39:15-39:16  V1
testdata/Builtins.lc 39:17-39:22  Type
testdata/Builtins.lc 39:26-39:29  Nat -> Type->Type
testdata/Builtins.lc 39:26-39:31  Type->Type
testdata/Builtins.lc 39:26-39:37  Type
testdata/Builtins.lc 39:26-39:84  Type
testdata/Builtins.lc 39:30-39:31  V1
testdata/Builtins.lc 39:32-39:37  Type
testdata/Builtins.lc 39:41-39:44  Nat -> Type->Type
testdata/Builtins.lc 39:41-39:46  Type->Type
testdata/Builtins.lc 39:41-39:52  Type
testdata/Builtins.lc 39:41-39:84  Type
testdata/Builtins.lc 39:45-39:46  V1
testdata/Builtins.lc 39:47-39:52  Type
testdata/Builtins.lc 39:56-39:59  Nat -> Type->Type
testdata/Builtins.lc 39:56-39:61  Type->Type
testdata/Builtins.lc 39:56-39:67  Type
testdata/Builtins.lc 39:56-39:84  Type
testdata/Builtins.lc 39:60-39:61  V1
testdata/Builtins.lc 39:62-39:67  Type
testdata/Builtins.lc 39:71-39:74  Nat -> Nat -> Type->Type
testdata/Builtins.lc 39:71-39:76  Nat -> Type->Type
testdata/Builtins.lc 39:71-39:78  Type->Type
testdata/Builtins.lc 39:71-39:84  Type
testdata/Builtins.lc 39:75-39:76  V1
testdata/Builtins.lc 39:75-39:78  a:Type -> Mat 2 4 a -> Type
testdata/Builtins.lc 39:75-39:84  Mat 2 4 Float -> Type
testdata/Builtins.lc 39:77-39:78  V1
testdata/Builtins.lc 39:79-39:84  Type
testdata/Builtins.lc 40:3-40:7  Mat 3 4 Float | Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Vec 3 Float -> Mat 3 4 Float
testdata/Builtins.lc 40:3-40:84  Type
testdata/Builtins.lc 40:11-40:14  Nat -> Type->Type
testdata/Builtins.lc 40:11-40:16  Type->Type
testdata/Builtins.lc 40:11-40:22  Type
testdata/Builtins.lc 40:15-40:16  V1
testdata/Builtins.lc 40:17-40:22  Type
testdata/Builtins.lc 40:26-40:29  Nat -> Type->Type
testdata/Builtins.lc 40:26-40:31  Type->Type
testdata/Builtins.lc 40:26-40:37  Type
testdata/Builtins.lc 40:26-40:84  Type
testdata/Builtins.lc 40:30-40:31  V1
testdata/Builtins.lc 40:32-40:37  Type
testdata/Builtins.lc 40:41-40:44  Nat -> Type->Type
testdata/Builtins.lc 40:41-40:46  Type->Type
testdata/Builtins.lc 40:41-40:52  Type
testdata/Builtins.lc 40:41-40:84  Type
testdata/Builtins.lc 40:45-40:46  V1
testdata/Builtins.lc 40:47-40:52  Type
testdata/Builtins.lc 40:56-40:59  Nat -> Type->Type
testdata/Builtins.lc 40:56-40:61  Type->Type
testdata/Builtins.lc 40:56-40:67  Type
testdata/Builtins.lc 40:56-40:84  Type
testdata/Builtins.lc 40:60-40:61  V1
testdata/Builtins.lc 40:62-40:67  Type
testdata/Builtins.lc 40:71-40:74  Nat -> Nat -> Type->Type
testdata/Builtins.lc 40:71-40:76  Nat -> Type->Type
testdata/Builtins.lc 40:71-40:78  Type->Type
testdata/Builtins.lc 40:71-40:84  Type
testdata/Builtins.lc 40:75-40:76  V1
testdata/Builtins.lc 40:75-40:78  a:Type -> Mat 3 4 a -> Type
testdata/Builtins.lc 40:75-40:84  Mat 3 4 Float -> Type
testdata/Builtins.lc 40:77-40:78  V1
testdata/Builtins.lc 40:79-40:84  Type
testdata/Builtins.lc 41:3-41:7  Mat 4 4 Float | Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Vec 4 Float -> Mat 4 4 Float
testdata/Builtins.lc 41:3-41:84  Type
testdata/Builtins.lc 41:11-41:14  Nat -> Type->Type
testdata/Builtins.lc 41:11-41:16  Type->Type
testdata/Builtins.lc 41:11-41:22  Type
testdata/Builtins.lc 41:15-41:16  V1
testdata/Builtins.lc 41:17-41:22  Type
testdata/Builtins.lc 41:26-41:29  Nat -> Type->Type
testdata/Builtins.lc 41:26-41:31  Type->Type
testdata/Builtins.lc 41:26-41:37  Type
testdata/Builtins.lc 41:26-41:84  Type
testdata/Builtins.lc 41:30-41:31  V1
testdata/Builtins.lc 41:32-41:37  Type
testdata/Builtins.lc 41:41-41:44  Nat -> Type->Type
testdata/Builtins.lc 41:41-41:46  Type->Type
testdata/Builtins.lc 41:41-41:52  Type
testdata/Builtins.lc 41:41-41:84  Type
testdata/Builtins.lc 41:45-41:46  V1
testdata/Builtins.lc 41:47-41:52  Type
testdata/Builtins.lc 41:56-41:59  Nat -> Type->Type
testdata/Builtins.lc 41:56-41:61  Type->Type
testdata/Builtins.lc 41:56-41:67  Type
testdata/Builtins.lc 41:56-41:84  Type
testdata/Builtins.lc 41:60-41:61  V1
testdata/Builtins.lc 41:62-41:67  Type
testdata/Builtins.lc 41:71-41:74  Nat -> Nat -> Type->Type
testdata/Builtins.lc 41:71-41:76  Nat -> Type->Type
testdata/Builtins.lc 41:71-41:78  Type->Type
testdata/Builtins.lc 41:71-41:84  Type
testdata/Builtins.lc 41:75-41:76  V1
testdata/Builtins.lc 41:75-41:78  a:Type -> Mat 4 4 a -> Type
testdata/Builtins.lc 41:75-41:84  Mat 4 4 Float -> Type
testdata/Builtins.lc 41:77-41:78  V1
testdata/Builtins.lc 41:79-41:84  Type
testdata/Builtins.lc 44:5-44:21  Type->Type
testdata/Builtins.lc 44:22-44:27  Type
testdata/Builtins.lc 44:22-44:35  Type->Type
testdata/Builtins.lc 44:22-48:37  Type | Type->Type
testdata/Builtins.lc 44:30-44:35  Type
testdata/Builtins.lc 45:22-45:26  Type
testdata/Builtins.lc 45:22-45:33  Type->Type
testdata/Builtins.lc 45:22-48:37  Type
testdata/Builtins.lc 45:29-45:33  Type
testdata/Builtins.lc 46:22-46:25  Type
testdata/Builtins.lc 46:22-46:31  Type->Type
testdata/Builtins.lc 46:22-48:37  Type
testdata/Builtins.lc 46:28-46:31  Type
testdata/Builtins.lc 47:23-47:27  Type
testdata/Builtins.lc 47:23-47:36  Type->Type
testdata/Builtins.lc 47:23-48:37  Type
testdata/Builtins.lc 47:35-47:36  Nat->Type | Type | Type -> Nat->Type
testdata/Builtins.lc 48:23-48:26  Type
testdata/Builtins.lc 48:23-48:37  Type->Type
testdata/Builtins.lc 48:36-48:37  Nat -> Nat -> Type->Type | Nat -> Type->Type | Type | Type->Type
testdata/Builtins.lc 52:7-52:13  Type->Type
testdata/Builtins.lc 54:25-54:28  Type
testdata/Builtins.lc 54:25-55:30  Type | Type->Type
testdata/Builtins.lc 55:25-55:30  Type
testdata/Builtins.lc 57:7-57:16  Type->Type
testdata/Builtins.lc 57:7-58:12  Type
testdata/Builtins.lc 57:7-59:11  Type
testdata/Builtins.lc 58:3-58:7  {a} -> {b : Component a}->a
testdata/Builtins.lc 58:11-58:12  Type
testdata/Builtins.lc 59:3-59:6  {a} -> {b : Component a}->a
testdata/Builtins.lc 59:10-59:11  Type
testdata/Builtins.lc 61:20-61:23  Type
testdata/Builtins.lc 61:20-62:18  V1->V2
testdata/Builtins.lc 61:20-63:17  V1->V2
testdata/Builtins.lc 61:20-79:24  Type | Type->Type
testdata/Builtins.lc 61:20-89:36  V1 | {a : Component V0}->V1 | {a} -> {b : Component a}->a
testdata/Builtins.lc 61:20-90:31  V1 | {a : Component V0}->V1 | {a} -> {b : Component a}->a
testdata/Builtins.lc 62:10-62:11  V1
testdata/Builtins.lc 62:15-62:18  Type
testdata/Builtins.lc 63:9-63:10  V1
testdata/Builtins.lc 63:14-63:17  Type
testdata/Builtins.lc 64:20-64:24  Type
testdata/Builtins.lc 64:20-65:19  V1->V2
testdata/Builtins.lc 64:20-66:18  V1->V2
testdata/Builtins.lc 64:20-79:24  Type
testdata/Builtins.lc 64:20-89:36  V1
testdata/Builtins.lc 64:20-90:31  V1
testdata/Builtins.lc 65:10-65:11  V1
testdata/Builtins.lc 65:15-65:19  Type
testdata/Builtins.lc 66:9-66:10  V1
testdata/Builtins.lc 66:14-66:18  Type
testdata/Builtins.lc 67:20-67:25  Type
testdata/Builtins.lc 67:20-68:13  V1->V2
testdata/Builtins.lc 67:20-69:12  V1->V2
testdata/Builtins.lc 67:20-79:24  Type
testdata/Builtins.lc 67:20-89:36  V1
testdata/Builtins.lc 67:20-90:31  V1
testdata/Builtins.lc 68:10-68:13  Float
testdata/Builtins.lc 69:9-69:12  Float
testdata/Builtins.lc 70:21-70:25  Type
testdata/Builtins.lc 70:21-79:24  Type
testdata/Builtins.lc 70:21-89:36  V1->V2
testdata/Builtins.lc 70:21-90:31  V1->V2
testdata/Builtins.lc 71:10-71:12  {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 71:10-71:16  Float -> VecS Float 2
testdata/Builtins.lc 71:10-71:20  VecS Float 2
testdata/Builtins.lc 71:10-77:28  a:Nat -> VecS Float ('Succ ('Succ a)) | a:Nat -> VecS Float ('Succ a)
testdata/Builtins.lc 71:10-89:36  VecS V1 V0 | a:Nat -> VecS V1 a | a:Type -> b:Nat -> VecS a b
testdata/Builtins.lc 71:13-71:16  Float
testdata/Builtins.lc 71:17-71:20  Float
testdata/Builtins.lc 72:9-72:11  {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 72:9-72:15  Float -> VecS Float 2
testdata/Builtins.lc 72:9-72:19  VecS Float 2
testdata/Builtins.lc 72:9-78:27  a:Nat -> VecS Float ('Succ ('Succ a)) | a:Nat -> VecS Float ('Succ a)
testdata/Builtins.lc 72:9-90:31  VecS V1 V0 | a:Nat -> VecS V1 a | a:Type -> b:Nat -> VecS a b
testdata/Builtins.lc 72:12-72:15  Float
testdata/Builtins.lc 72:16-72:19  Float
testdata/Builtins.lc 74:10-74:12  {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 74:10-74:16  Float -> Float -> VecS Float 3
testdata/Builtins.lc 74:10-74:20  Float -> VecS Float 3
testdata/Builtins.lc 74:10-74:24  VecS Float 3
testdata/Builtins.lc 74:10-77:28  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
testdata/Builtins.lc 74:13-74:16  Float
testdata/Builtins.lc 74:17-74:20  Float
testdata/Builtins.lc 74:21-74:24  Float
testdata/Builtins.lc 75:9-75:11  {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 75:9-75:15  Float -> Float -> VecS Float 3
testdata/Builtins.lc 75:9-75:19  Float -> VecS Float 3
testdata/Builtins.lc 75:9-75:23  VecS Float 3
testdata/Builtins.lc 75:9-78:27  a:Nat -> VecS Float ('Succ ('Succ ('Succ a)))
testdata/Builtins.lc 75:12-75:15  Float
testdata/Builtins.lc 75:16-75:19  Float
testdata/Builtins.lc 75:20-75:23  Float
testdata/Builtins.lc 77:10-77:12  {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 77:10-77:16  Float -> Float -> Float -> VecS Float 4
testdata/Builtins.lc 77:10-77:20  Float -> Float -> VecS Float 4
testdata/Builtins.lc 77:10-77:24  Float -> VecS Float 4
testdata/Builtins.lc 77:10-77:28  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
testdata/Builtins.lc 77:13-77:16  Float
testdata/Builtins.lc 77:17-77:20  Float
testdata/Builtins.lc 77:21-77:24  Float
testdata/Builtins.lc 77:25-77:28  Float
testdata/Builtins.lc 78:9-78:11  {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 78:9-78:15  Float -> Float -> Float -> VecS Float 4
testdata/Builtins.lc 78:9-78:19  Float -> Float -> VecS Float 4
testdata/Builtins.lc 78:9-78:23  Float -> VecS Float 4
testdata/Builtins.lc 78:9-78:27  VecS Float 4 | a:Nat -> VecS Float ('Succ ('Succ ('Succ ('Succ a))))
testdata/Builtins.lc 78:12-78:15  Float
testdata/Builtins.lc 78:16-78:19  Float
testdata/Builtins.lc 78:20-78:23  Float
testdata/Builtins.lc 78:24-78:27  Float
testdata/Builtins.lc 79:20-79:24  Type
testdata/Builtins.lc 79:20-80:15  V1->V2
testdata/Builtins.lc 79:20-81:13  V1->V2
testdata/Builtins.lc 80:10-80:15  Bool
testdata/Builtins.lc 81:9-81:13  Bool
testdata/Builtins.lc 83:10-83:12  {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 83:10-83:18  Bool -> VecS Bool 2
testdata/Builtins.lc 83:10-83:24  VecS Bool 2
testdata/Builtins.lc 83:10-89:36  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
testdata/Builtins.lc 83:13-83:18  Bool
testdata/Builtins.lc 83:19-83:24  Bool
testdata/Builtins.lc 84:9-84:11  {a} -> a -> a -> VecS a 2
testdata/Builtins.lc 84:9-84:16  Bool -> VecS Bool 2
testdata/Builtins.lc 84:9-84:21  VecS Bool 2
testdata/Builtins.lc 84:9-90:31  a:Nat -> VecS Bool ('Succ ('Succ a)) | a:Nat -> VecS Bool ('Succ a)
testdata/Builtins.lc 84:12-84:16  Bool
testdata/Builtins.lc 84:17-84:21  Bool
testdata/Builtins.lc 86:10-86:12  {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 86:10-86:18  Bool -> Bool -> VecS Bool 3
testdata/Builtins.lc 86:10-86:24  Bool -> VecS Bool 3
testdata/Builtins.lc 86:10-86:30  VecS Bool 3
testdata/Builtins.lc 86:10-89:36  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
testdata/Builtins.lc 86:13-86:18  Bool
testdata/Builtins.lc 86:19-86:24  Bool
testdata/Builtins.lc 86:25-86:30  Bool
testdata/Builtins.lc 87:9-87:11  {a} -> a -> a -> a -> VecS a 3
testdata/Builtins.lc 87:9-87:16  Bool -> Bool -> VecS Bool 3
testdata/Builtins.lc 87:9-87:21  Bool -> VecS Bool 3
testdata/Builtins.lc 87:9-87:26  VecS Bool 3
testdata/Builtins.lc 87:9-90:31  a:Nat -> VecS Bool ('Succ ('Succ ('Succ a)))
testdata/Builtins.lc 87:12-87:16  Bool
testdata/Builtins.lc 87:17-87:21  Bool
testdata/Builtins.lc 87:22-87:26  Bool
testdata/Builtins.lc 89:10-89:12  {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 89:10-89:18  Bool -> Bool -> Bool -> VecS Bool 4
testdata/Builtins.lc 89:10-89:24  Bool -> Bool -> VecS Bool 4
testdata/Builtins.lc 89:10-89:30  Bool -> VecS Bool 4
testdata/Builtins.lc 89:10-89:36  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
testdata/Builtins.lc 89:13-89:18  Bool
testdata/Builtins.lc 89:19-89:24  Bool
testdata/Builtins.lc 89:25-89:30  Bool
testdata/Builtins.lc 89:31-89:36  Bool
testdata/Builtins.lc 90:9-90:11  {a} -> a -> a -> a -> a -> VecS a 4
testdata/Builtins.lc 90:9-90:16  Bool -> Bool -> Bool -> VecS Bool 4
testdata/Builtins.lc 90:9-90:21  Bool -> Bool -> VecS Bool 4
testdata/Builtins.lc 90:9-90:26  Bool -> VecS Bool 4
testdata/Builtins.lc 90:9-90:31  VecS Bool 4 | a:Nat -> VecS Bool ('Succ ('Succ ('Succ ('Succ a))))
testdata/Builtins.lc 90:12-90:16  Bool
testdata/Builtins.lc 90:17-90:21  Bool
testdata/Builtins.lc 90:22-90:26  Bool
testdata/Builtins.lc 90:27-90:31  Bool
testdata/Builtins.lc 92:7-92:15  Type->Type
testdata/Builtins.lc 94:25-94:28  Type
testdata/Builtins.lc 94:25-95:29  Type | Type->Type
testdata/Builtins.lc 95:25-95:29  Type
testdata/Builtins.lc 97:7-97:15  Type->Type
testdata/Builtins.lc 99:25-99:30  Type
testdata/Builtins.lc 99:25-103:29  Type | Type->Type
testdata/Builtins.lc 100:26-100:30  Type
testdata/Builtins.lc 100:26-103:29  Type
testdata/Builtins.lc 103:26-103:29  Type
testdata/Builtins.lc 118:1-118:8  {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
testdata/Builtins.lc 118:10-118:17  {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
testdata/Builtins.lc 118:19-118:26  {a} -> {b : Num (MatVecScalarElem a)} -> a -> a->a
testdata/Builtins.lc 118:34-118:37  Type->Type
testdata/Builtins.lc 118:34-118:58  Type
testdata/Builtins.lc 118:34-118:73  Type
testdata/Builtins.lc 118:39-118:55  Type->Type
testdata/Builtins.lc 118:39-118:57  Type
testdata/Builtins.lc 118:56-118:57  V1
testdata/Builtins.lc 118:62-118:63  Type
testdata/Builtins.lc 118:62-118:73  Type
testdata/Builtins.lc 118:67-118:68  Type
testdata/Builtins.lc 118:67-118:73  Type
testdata/Builtins.lc 118:72-118:73  Type
testdata/Builtins.lc 119:1-119:9  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
testdata/Builtins.lc 119:11-119:19  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
testdata/Builtins.lc 119:21-119:29  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
testdata/Builtins.lc 119:34-119:80  Type
testdata/Builtins.lc 119:35-119:36  V4
testdata/Builtins.lc 119:35-119:38  V3->Type
testdata/Builtins.lc 119:35-119:57  Type
testdata/Builtins.lc 119:37-119:38  {a} -> a -> a->Type
testdata/Builtins.lc 119:39-119:55  Type->Type
testdata/Builtins.lc 119:39-119:57  Type
testdata/Builtins.lc 119:56-119:57  V1
testdata/Builtins.lc 119:59-119:62  Type->Type
testdata/Builtins.lc 119:59-119:64  Type
testdata/Builtins.lc 119:59-119:80  Type
testdata/Builtins.lc 119:63-119:64  Type
testdata/Builtins.lc 119:69-119:70  Type
testdata/Builtins.lc 119:69-119:80  Type
testdata/Builtins.lc 119:74-119:75  Type
testdata/Builtins.lc 119:74-119:80  Type
testdata/Builtins.lc 119:79-119:80  Type
testdata/Builtins.lc 120:1-120:8  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 120:10-120:17  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 120:34-120:75  Type
testdata/Builtins.lc 120:35-120:38  Type->Type
testdata/Builtins.lc 120:35-120:40  Type
testdata/Builtins.lc 120:39-120:40  V5
testdata/Builtins.lc 120:42-120:43  V5
testdata/Builtins.lc 120:42-120:45  V4->Type
testdata/Builtins.lc 120:42-120:59  Type
testdata/Builtins.lc 120:42-120:75  Type
testdata/Builtins.lc 120:44-120:45  {a} -> a -> a->Type
testdata/Builtins.lc 120:46-120:55  Nat -> Type->Type
testdata/Builtins.lc 120:46-120:57  Type->Type
testdata/Builtins.lc 120:46-120:59  Type
testdata/Builtins.lc 120:56-120:57  V2
testdata/Builtins.lc 120:58-120:59  Type
testdata/Builtins.lc 120:64-120:65  Type
testdata/Builtins.lc 120:64-120:75  Type
testdata/Builtins.lc 120:69-120:70  Type
testdata/Builtins.lc 120:69-120:75  Type
testdata/Builtins.lc 120:74-120:75  Type
testdata/Builtins.lc 121:1-121:9  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 121:11-121:19  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 121:34-121:75  Type
testdata/Builtins.lc 121:35-121:38  Type->Type
testdata/Builtins.lc 121:35-121:40  Type
testdata/Builtins.lc 121:39-121:40  V5
testdata/Builtins.lc 121:42-121:43  V5
testdata/Builtins.lc 121:42-121:45  V4->Type
testdata/Builtins.lc 121:42-121:59  Type
testdata/Builtins.lc 121:42-121:75  Type
testdata/Builtins.lc 121:44-121:45  {a} -> a -> a->Type
testdata/Builtins.lc 121:46-121:55  Nat -> Type->Type
testdata/Builtins.lc 121:46-121:57  Type->Type
testdata/Builtins.lc 121:46-121:59  Type
testdata/Builtins.lc 121:56-121:57  V2
testdata/Builtins.lc 121:58-121:59  Type
testdata/Builtins.lc 121:64-121:65  Type
testdata/Builtins.lc 121:64-121:75  Type
testdata/Builtins.lc 121:69-121:70  Type
testdata/Builtins.lc 121:69-121:75  Type
testdata/Builtins.lc 121:74-121:75  Type
testdata/Builtins.lc 122:1-122:8  {a} -> {b : Signed (MatVecScalarElem a)} -> a->a
testdata/Builtins.lc 122:34-122:40  Type->Type
testdata/Builtins.lc 122:34-122:61  Type
testdata/Builtins.lc 122:34-122:71  Type
testdata/Builtins.lc 122:42-122:58  Type->Type
testdata/Builtins.lc 122:42-122:60  Type
testdata/Builtins.lc 122:59-122:60  V1
testdata/Builtins.lc 122:65-122:66  Type
testdata/Builtins.lc 122:65-122:71  Type
testdata/Builtins.lc 122:70-122:71  Type
testdata/Builtins.lc 124:1-124:9  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 124:11-124:18  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 124:20-124:28  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 124:34-124:80  Type
testdata/Builtins.lc 124:35-124:43  Type->Type
testdata/Builtins.lc 124:35-124:45  Type
testdata/Builtins.lc 124:44-124:45  V5
testdata/Builtins.lc 124:47-124:48  V5
testdata/Builtins.lc 124:47-124:50  V4->Type
testdata/Builtins.lc 124:47-124:64  Type
testdata/Builtins.lc 124:47-124:80  Type
testdata/Builtins.lc 124:49-124:50  {a} -> a -> a->Type
testdata/Builtins.lc 124:51-124:60  Nat -> Type->Type
testdata/Builtins.lc 124:51-124:62  Type->Type
testdata/Builtins.lc 124:51-124:64  Type
testdata/Builtins.lc 124:61-124:62  V2
testdata/Builtins.lc 124:63-124:64  Type
testdata/Builtins.lc 124:69-124:70  Type
testdata/Builtins.lc 124:69-124:80  Type
testdata/Builtins.lc 124:74-124:75  Type
testdata/Builtins.lc 124:74-124:80  Type
testdata/Builtins.lc 124:79-124:80  Type
testdata/Builtins.lc 125:1-125:10  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 125:12-125:20  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 125:22-125:31  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 125:34-125:80  Type
testdata/Builtins.lc 125:35-125:43  Type->Type
testdata/Builtins.lc 125:35-125:45  Type
testdata/Builtins.lc 125:44-125:45  V5
testdata/Builtins.lc 125:47-125:48  V5
testdata/Builtins.lc 125:47-125:50  V4->Type
testdata/Builtins.lc 125:47-125:64  Type
testdata/Builtins.lc 125:47-125:80  Type
testdata/Builtins.lc 125:49-125:50  {a} -> a -> a->Type
testdata/Builtins.lc 125:51-125:60  Nat -> Type->Type
testdata/Builtins.lc 125:51-125:62  Type->Type
testdata/Builtins.lc 125:51-125:64  Type
testdata/Builtins.lc 125:61-125:62  V2
testdata/Builtins.lc 125:63-125:64  Type
testdata/Builtins.lc 125:69-125:70  Type
testdata/Builtins.lc 125:69-125:80  Type
testdata/Builtins.lc 125:74-125:75  Type
testdata/Builtins.lc 125:74-125:80  Type
testdata/Builtins.lc 125:79-125:80  Type
testdata/Builtins.lc 126:1-126:9  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b->b
testdata/Builtins.lc 126:34-126:75  Type
testdata/Builtins.lc 126:35-126:43  Type->Type
testdata/Builtins.lc 126:35-126:45  Type
testdata/Builtins.lc 126:44-126:45  V5
testdata/Builtins.lc 126:47-126:48  V5
testdata/Builtins.lc 126:47-126:50  V4->Type
testdata/Builtins.lc 126:47-126:64  Type
testdata/Builtins.lc 126:47-126:75  Type
testdata/Builtins.lc 126:49-126:50  {a} -> a -> a->Type
testdata/Builtins.lc 126:51-126:60  Nat -> Type->Type
testdata/Builtins.lc 126:51-126:62  Type->Type
testdata/Builtins.lc 126:51-126:64  Type
testdata/Builtins.lc 126:61-126:62  V2
testdata/Builtins.lc 126:63-126:64  Type
testdata/Builtins.lc 126:69-126:70  Type
testdata/Builtins.lc 126:69-126:75  Type
testdata/Builtins.lc 126:74-126:75  Type
testdata/Builtins.lc 127:1-127:12  {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b
testdata/Builtins.lc 127:14-127:25  {a} -> {b} -> {c:Nat} -> {d} -> {e : Integral a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Word} -> b -> d->b
testdata/Builtins.lc 127:34-127:102  Type
testdata/Builtins.lc 127:35-127:43  Type->Type
testdata/Builtins.lc 127:35-127:45  Type
testdata/Builtins.lc 127:44-127:45  V7
testdata/Builtins.lc 127:47-127:48  V7
testdata/Builtins.lc 127:47-127:50  V6->Type
testdata/Builtins.lc 127:47-127:64  Type
testdata/Builtins.lc 127:47-127:102  Type
testdata/Builtins.lc 127:49-127:50  {a} -> a -> a->Type
testdata/Builtins.lc 127:51-127:60  Nat -> Type->Type
testdata/Builtins.lc 127:51-127:62  Type->Type
testdata/Builtins.lc 127:51-127:64  Type
testdata/Builtins.lc 127:61-127:62  V4
testdata/Builtins.lc 127:63-127:64  Type
testdata/Builtins.lc 127:66-127:67  V4
testdata/Builtins.lc 127:66-127:69  V3->Type
testdata/Builtins.lc 127:66-127:86  Type
testdata/Builtins.lc 127:66-127:102  Type
testdata/Builtins.lc 127:68-127:69  {a} -> a -> a->Type
testdata/Builtins.lc 127:70-127:79  Nat -> Type->Type
testdata/Builtins.lc 127:70-127:81  Type->Type
testdata/Builtins.lc 127:70-127:86  Type
testdata/Builtins.lc 127:80-127:81  Nat
testdata/Builtins.lc 127:82-127:86  Type
testdata/Builtins.lc 127:91-127:92  Type
testdata/Builtins.lc 127:91-127:102  Type
testdata/Builtins.lc 127:96-127:97  Type
testdata/Builtins.lc 127:96-127:102  Type
testdata/Builtins.lc 127:101-127:102  Type
testdata/Builtins.lc 128:1-128:13  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
testdata/Builtins.lc 128:15-128:27  {a} -> {b} -> {c:Nat} -> {d : Integral a} -> {e : b ~ VecScalar c a} -> b -> Word->b
testdata/Builtins.lc 128:34-128:83  Type
testdata/Builtins.lc 128:35-128:43  Type->Type
testdata/Builtins.lc 128:35-128:45  Type
testdata/Builtins.lc 128:44-128:45  V5
testdata/Builtins.lc 128:47-128:48  V5
testdata/Builtins.lc 128:47-128:50  V4->Type
testdata/Builtins.lc 128:47-128:64  Type
testdata/Builtins.lc 128:47-128:83  Type
testdata/Builtins.lc 128:49-128:50  {a} -> a -> a->Type
testdata/Builtins.lc 128:51-128:60  Nat -> Type->Type
testdata/Builtins.lc 128:51-128:62  Type->Type
testdata/Builtins.lc 128:51-128:64  Type
testdata/Builtins.lc 128:61-128:62  V2
testdata/Builtins.lc 128:63-128:64  Type
testdata/Builtins.lc 128:69-128:70  Type
testdata/Builtins.lc 128:69-128:83  Type
testdata/Builtins.lc 128:74-128:78  Type
testdata/Builtins.lc 128:74-128:83  Type
testdata/Builtins.lc 128:82-128:83  Type
testdata/Builtins.lc 130:1-130:8  Bool -> Bool->Bool
testdata/Builtins.lc 130:10-130:16  Bool -> Bool->Bool
testdata/Builtins.lc 130:18-130:25  Bool -> Bool->Bool
testdata/Builtins.lc 130:34-130:38  Type
testdata/Builtins.lc 130:42-130:46  Type
testdata/Builtins.lc 130:42-130:54  Type
testdata/Builtins.lc 130:50-130:54  Type
testdata/Builtins.lc 131:1-131:8  {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a
testdata/Builtins.lc 131:47-131:79  Type
testdata/Builtins.lc 131:48-131:49  V4
testdata/Builtins.lc 131:48-131:51  V3->Type
testdata/Builtins.lc 131:48-131:68  Type
testdata/Builtins.lc 131:50-131:51  {a} -> a -> a->Type
testdata/Builtins.lc 131:52-131:61  Nat -> Type->Type
testdata/Builtins.lc 131:52-131:63  Type->Type
testdata/Builtins.lc 131:52-131:68  Type
testdata/Builtins.lc 131:62-131:63  V1
testdata/Builtins.lc 131:64-131:68  Type
testdata/Builtins.lc 131:73-131:74  Type
testdata/Builtins.lc 131:73-131:79  Type
testdata/Builtins.lc 131:78-131:79  Type
testdata/Builtins.lc 132:1-132:8  {a:Nat} -> VecScalar a Bool -> Bool
testdata/Builtins.lc 132:10-132:17  {a:Nat} -> VecScalar a Bool -> Bool
testdata/Builtins.lc 132:34-132:43  Nat -> Type->Type
testdata/Builtins.lc 132:34-132:45  Type->Type
testdata/Builtins.lc 132:34-132:50  Type
testdata/Builtins.lc 132:34-132:58  Type
testdata/Builtins.lc 132:44-132:45  V1
testdata/Builtins.lc 132:46-132:50  Type
testdata/Builtins.lc 132:54-132:58  Type
testdata/Builtins.lc 135:1-135:9  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:11-135:20  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:22-135:30  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:32-135:41  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:43-135:51  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:53-135:62  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:64-135:71  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:73-135:81  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:83-135:94  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:96-135:107  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:109-135:116  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:118-135:126  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:128-135:135  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:137-135:145  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:147-135:154  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:156-135:163  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:165-135:173  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:175-135:183  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:185-135:193  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 135:195-135:206  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 136:34-136:67  Type
testdata/Builtins.lc 136:35-136:36  V4
testdata/Builtins.lc 136:35-136:38  V3->Type
testdata/Builtins.lc 136:35-136:56  Type
testdata/Builtins.lc 136:37-136:38  {a} -> a -> a->Type
testdata/Builtins.lc 136:39-136:48  Nat -> Type->Type
testdata/Builtins.lc 136:39-136:50  Type->Type
testdata/Builtins.lc 136:39-136:56  Type
testdata/Builtins.lc 136:49-136:50  V1
testdata/Builtins.lc 136:51-136:56  Type
testdata/Builtins.lc 136:61-136:62  Type
testdata/Builtins.lc 136:61-136:67  Type
testdata/Builtins.lc 136:66-136:67  Type
testdata/Builtins.lc 137:1-137:8  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
testdata/Builtins.lc 137:10-137:19  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
testdata/Builtins.lc 137:34-137:72  Type
testdata/Builtins.lc 137:35-137:36  V4
testdata/Builtins.lc 137:35-137:38  V3->Type
testdata/Builtins.lc 137:35-137:56  Type
testdata/Builtins.lc 137:37-137:38  {a} -> a -> a->Type
testdata/Builtins.lc 137:39-137:48  Nat -> Type->Type
testdata/Builtins.lc 137:39-137:50  Type->Type
testdata/Builtins.lc 137:39-137:56  Type
testdata/Builtins.lc 137:49-137:50  V1
testdata/Builtins.lc 137:51-137:56  Type
testdata/Builtins.lc 137:61-137:62  Type
testdata/Builtins.lc 137:61-137:72  Type
testdata/Builtins.lc 137:66-137:67  Type
testdata/Builtins.lc 137:66-137:72  Type
testdata/Builtins.lc 137:71-137:72  Type
testdata/Builtins.lc 139:1-139:10  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 139:12-139:21  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 139:23-139:32  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 139:34-139:47  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 139:49-139:57  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 139:59-139:68  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 140:34-140:67  Type
testdata/Builtins.lc 140:35-140:36  V4
testdata/Builtins.lc 140:35-140:38  V3->Type
testdata/Builtins.lc 140:35-140:56  Type
testdata/Builtins.lc 140:37-140:38  {a} -> a -> a->Type
testdata/Builtins.lc 140:39-140:48  Nat -> Type->Type
testdata/Builtins.lc 140:39-140:50  Type->Type
testdata/Builtins.lc 140:39-140:56  Type
testdata/Builtins.lc 140:49-140:50  V1
testdata/Builtins.lc 140:51-140:56  Type
testdata/Builtins.lc 140:61-140:62  Type
testdata/Builtins.lc 140:61-140:67  Type
testdata/Builtins.lc 140:66-140:67  Type
testdata/Builtins.lc 141:1-141:8  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 141:10-141:17  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b->b
testdata/Builtins.lc 141:34-141:75  Type
testdata/Builtins.lc 141:35-141:38  Type->Type
testdata/Builtins.lc 141:35-141:40  Type
testdata/Builtins.lc 141:39-141:40  V5
testdata/Builtins.lc 141:42-141:43  V5
testdata/Builtins.lc 141:42-141:45  V4->Type
testdata/Builtins.lc 141:42-141:59  Type
testdata/Builtins.lc 141:42-141:75  Type
testdata/Builtins.lc 141:44-141:45  {a} -> a -> a->Type
testdata/Builtins.lc 141:46-141:55  Nat -> Type->Type
testdata/Builtins.lc 141:46-141:57  Type->Type
testdata/Builtins.lc 141:46-141:59  Type
testdata/Builtins.lc 141:56-141:57  V2
testdata/Builtins.lc 141:58-141:59  Type
testdata/Builtins.lc 141:64-141:65  Type
testdata/Builtins.lc 141:64-141:75  Type
testdata/Builtins.lc 141:69-141:70  Type
testdata/Builtins.lc 141:69-141:75  Type
testdata/Builtins.lc 141:74-141:75  Type
testdata/Builtins.lc 142:1-142:9  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 142:11-142:19  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a->b
testdata/Builtins.lc 142:34-142:75  Type
testdata/Builtins.lc 142:35-142:38  Type->Type
testdata/Builtins.lc 142:35-142:40  Type
testdata/Builtins.lc 142:39-142:40  V5
testdata/Builtins.lc 142:42-142:43  V5
testdata/Builtins.lc 142:42-142:45  V4->Type
testdata/Builtins.lc 142:42-142:59  Type
testdata/Builtins.lc 142:42-142:75  Type
testdata/Builtins.lc 142:44-142:45  {a} -> a -> a->Type
testdata/Builtins.lc 142:46-142:55  Nat -> Type->Type
testdata/Builtins.lc 142:46-142:57  Type->Type
testdata/Builtins.lc 142:46-142:59  Type
testdata/Builtins.lc 142:56-142:57  V2
testdata/Builtins.lc 142:58-142:59  Type
testdata/Builtins.lc 142:64-142:65  Type
testdata/Builtins.lc 142:64-142:75  Type
testdata/Builtins.lc 142:69-142:70  Type
testdata/Builtins.lc 142:69-142:75  Type
testdata/Builtins.lc 142:74-142:75  Type
testdata/Builtins.lc 143:1-143:10  {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c
testdata/Builtins.lc 143:12-143:21  {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c
testdata/Builtins.lc 143:34-143:89  Type
testdata/Builtins.lc 143:35-143:36  V6
testdata/Builtins.lc 143:35-143:38  V5->Type
testdata/Builtins.lc 143:35-143:56  Type
testdata/Builtins.lc 143:37-143:38  {a} -> a -> a->Type
testdata/Builtins.lc 143:39-143:48  Nat -> Type->Type
testdata/Builtins.lc 143:39-143:50  Type->Type
testdata/Builtins.lc 143:39-143:56  Type
testdata/Builtins.lc 143:49-143:50  V3
testdata/Builtins.lc 143:51-143:56  Type
testdata/Builtins.lc 143:58-143:59  V3
testdata/Builtins.lc 143:58-143:61  V2->Type
testdata/Builtins.lc 143:58-143:78  Type
testdata/Builtins.lc 143:58-143:89  Type
testdata/Builtins.lc 143:60-143:61  {a} -> a -> a->Type
testdata/Builtins.lc 143:62-143:71  Nat -> Type->Type
testdata/Builtins.lc 143:62-143:73  Type->Type
testdata/Builtins.lc 143:62-143:78  Type
testdata/Builtins.lc 143:72-143:73  Nat
testdata/Builtins.lc 143:74-143:78  Type
testdata/Builtins.lc 143:83-143:84  Type
testdata/Builtins.lc 143:83-143:89  Type
testdata/Builtins.lc 143:88-143:89  Type
testdata/Builtins.lc 144:1-144:8  {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b
testdata/Builtins.lc 144:10-144:18  {a} -> {b} -> {c:Nat} -> {d : Signed a} -> {e : b ~ VecScalar c a} -> b->b
testdata/Builtins.lc 144:34-144:73  Type
testdata/Builtins.lc 144:35-144:41  Type->Type
testdata/Builtins.lc 144:35-144:43  Type
testdata/Builtins.lc 144:42-144:43  V5
testdata/Builtins.lc 144:45-144:46  V5
testdata/Builtins.lc 144:45-144:48  V4->Type
testdata/Builtins.lc 144:45-144:62  Type
testdata/Builtins.lc 144:45-144:73  Type
testdata/Builtins.lc 144:47-144:48  {a} -> a -> a->Type
testdata/Builtins.lc 144:49-144:58  Nat -> Type->Type
testdata/Builtins.lc 144:49-144:60  Type->Type
testdata/Builtins.lc 144:49-144:62  Type
testdata/Builtins.lc 144:59-144:60  V2
testdata/Builtins.lc 144:61-144:62  Type
testdata/Builtins.lc 144:67-144:68  Type
testdata/Builtins.lc 144:67-144:73  Type
testdata/Builtins.lc 144:72-144:73  Type
testdata/Builtins.lc 145:1-145:9  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->(a, a)
testdata/Builtins.lc 145:34-145:72  Type
testdata/Builtins.lc 145:35-145:36  V4
testdata/Builtins.lc 145:35-145:38  V3->Type
testdata/Builtins.lc 145:35-145:56  Type
testdata/Builtins.lc 145:37-145:38  {a} -> a -> a->Type
testdata/Builtins.lc 145:39-145:48  Nat -> Type->Type
testdata/Builtins.lc 145:39-145:50  Type->Type
testdata/Builtins.lc 145:39-145:56  Type
testdata/Builtins.lc 145:49-145:50  V1
testdata/Builtins.lc 145:51-145:56  Type
testdata/Builtins.lc 145:61-145:62  Type
testdata/Builtins.lc 145:61-145:72  Type
testdata/Builtins.lc 145:66-145:72  Type
testdata/Builtins.lc 145:67-145:68  Type
testdata/Builtins.lc 145:67-145:71  List Type
testdata/Builtins.lc 145:70-145:71  List Type | Type
testdata/Builtins.lc 146:1-146:10  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> b -> b->b
testdata/Builtins.lc 146:34-146:80  Type
testdata/Builtins.lc 146:35-146:38  Type->Type
testdata/Builtins.lc 146:35-146:40  Type
testdata/Builtins.lc 146:39-146:40  V5
testdata/Builtins.lc 146:42-146:43  V5
testdata/Builtins.lc 146:42-146:45  V4->Type
testdata/Builtins.lc 146:42-146:59  Type
testdata/Builtins.lc 146:42-146:80  Type
testdata/Builtins.lc 146:44-146:45  {a} -> a -> a->Type
testdata/Builtins.lc 146:46-146:55  Nat -> Type->Type
testdata/Builtins.lc 146:46-146:57  Type->Type
testdata/Builtins.lc 146:46-146:59  Type
testdata/Builtins.lc 146:56-146:57  V2
testdata/Builtins.lc 146:58-146:59  Type
testdata/Builtins.lc 146:64-146:65  Type
testdata/Builtins.lc 146:64-146:80  Type
testdata/Builtins.lc 146:69-146:70  Type
testdata/Builtins.lc 146:69-146:80  Type
testdata/Builtins.lc 146:74-146:75  Type
testdata/Builtins.lc 146:74-146:80  Type
testdata/Builtins.lc 146:79-146:80  Type
testdata/Builtins.lc 147:1-147:11  {a} -> {b} -> {c:Nat} -> {d : Num a} -> {e : b ~ VecScalar c a} -> b -> a -> a->b
testdata/Builtins.lc 147:34-147:80  Type
testdata/Builtins.lc 147:35-147:38  Type->Type
testdata/Builtins.lc 147:35-147:40  Type
testdata/Builtins.lc 147:39-147:40  V5
testdata/Builtins.lc 147:42-147:43  V5
testdata/Builtins.lc 147:42-147:45  V4->Type
testdata/Builtins.lc 147:42-147:59  Type
testdata/Builtins.lc 147:42-147:80  Type
testdata/Builtins.lc 147:44-147:45  {a} -> a -> a->Type
testdata/Builtins.lc 147:46-147:55  Nat -> Type->Type
testdata/Builtins.lc 147:46-147:57  Type->Type
testdata/Builtins.lc 147:46-147:59  Type
testdata/Builtins.lc 147:56-147:57  V2
testdata/Builtins.lc 147:58-147:59  Type
testdata/Builtins.lc 147:64-147:65  Type
testdata/Builtins.lc 147:64-147:80  Type
testdata/Builtins.lc 147:69-147:70  Type
testdata/Builtins.lc 147:69-147:80  Type
testdata/Builtins.lc 147:74-147:75  Type
testdata/Builtins.lc 147:74-147:80  Type
testdata/Builtins.lc 147:79-147:80  Type
testdata/Builtins.lc 148:1-148:8  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
testdata/Builtins.lc 148:34-148:77  Type
testdata/Builtins.lc 148:35-148:36  V4
testdata/Builtins.lc 148:35-148:38  V3->Type
testdata/Builtins.lc 148:35-148:56  Type
testdata/Builtins.lc 148:37-148:38  {a} -> a -> a->Type
testdata/Builtins.lc 148:39-148:48  Nat -> Type->Type
testdata/Builtins.lc 148:39-148:50  Type->Type
testdata/Builtins.lc 148:39-148:56  Type
testdata/Builtins.lc 148:49-148:50  V1
testdata/Builtins.lc 148:51-148:56  Type
testdata/Builtins.lc 148:61-148:62  Type
testdata/Builtins.lc 148:61-148:77  Type
testdata/Builtins.lc 148:66-148:67  Type
testdata/Builtins.lc 148:66-148:77  Type
testdata/Builtins.lc 148:71-148:72  Type
testdata/Builtins.lc 148:71-148:77  Type
testdata/Builtins.lc 148:76-148:77  Type
testdata/Builtins.lc 149:1-149:9  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> Float->a
testdata/Builtins.lc 149:34-149:81  Type
testdata/Builtins.lc 149:35-149:36  V4
testdata/Builtins.lc 149:35-149:38  V3->Type
testdata/Builtins.lc 149:35-149:56  Type
testdata/Builtins.lc 149:37-149:38  {a} -> a -> a->Type
testdata/Builtins.lc 149:39-149:48  Nat -> Type->Type
testdata/Builtins.lc 149:39-149:50  Type->Type
testdata/Builtins.lc 149:39-149:56  Type
testdata/Builtins.lc 149:49-149:50  V1
testdata/Builtins.lc 149:51-149:56  Type
testdata/Builtins.lc 149:61-149:62  Type
testdata/Builtins.lc 149:61-149:81  Type
testdata/Builtins.lc 149:66-149:67  Type
testdata/Builtins.lc 149:66-149:81  Type
testdata/Builtins.lc 149:71-149:76  Type
testdata/Builtins.lc 149:71-149:81  Type
testdata/Builtins.lc 149:80-149:81  Type
testdata/Builtins.lc 150:1-150:9  {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a
testdata/Builtins.lc 150:34-150:99  Type
testdata/Builtins.lc 150:35-150:36  V6
testdata/Builtins.lc 150:35-150:38  V5->Type
testdata/Builtins.lc 150:35-150:56  Type
testdata/Builtins.lc 150:37-150:38  {a} -> a -> a->Type
testdata/Builtins.lc 150:39-150:48  Nat -> Type->Type
testdata/Builtins.lc 150:39-150:50  Type->Type
testdata/Builtins.lc 150:39-150:56  Type
testdata/Builtins.lc 150:49-150:50  V3
testdata/Builtins.lc 150:51-150:56  Type
testdata/Builtins.lc 150:58-150:59  V3
testdata/Builtins.lc 150:58-150:61  V2->Type
testdata/Builtins.lc 150:58-150:78  Type
testdata/Builtins.lc 150:58-150:99  Type
testdata/Builtins.lc 150:60-150:61  {a} -> a -> a->Type
testdata/Builtins.lc 150:62-150:71  Nat -> Type->Type
testdata/Builtins.lc 150:62-150:73  Type->Type
testdata/Builtins.lc 150:62-150:78  Type
testdata/Builtins.lc 150:72-150:73  Nat
testdata/Builtins.lc 150:74-150:78  Type
testdata/Builtins.lc 150:83-150:84  Type
testdata/Builtins.lc 150:83-150:99  Type
testdata/Builtins.lc 150:88-150:89  Type
testdata/Builtins.lc 150:88-150:99  Type
testdata/Builtins.lc 150:93-150:94  Type
testdata/Builtins.lc 150:93-150:99  Type
testdata/Builtins.lc 150:98-150:99  Type
testdata/Builtins.lc 151:1-151:9  {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a->a
testdata/Builtins.lc 151:34-151:66  Type
testdata/Builtins.lc 151:35-151:36  V4
testdata/Builtins.lc 151:35-151:38  V3->Type
testdata/Builtins.lc 151:35-151:50  Type
testdata/Builtins.lc 151:37-151:38  {a} -> a -> a->Type
testdata/Builtins.lc 151:39-151:42  Nat -> Type->Type
testdata/Builtins.lc 151:39-151:44  Type->Type
testdata/Builtins.lc 151:39-151:50  Type
testdata/Builtins.lc 151:43-151:44  V1
testdata/Builtins.lc 151:45-151:50  Type
testdata/Builtins.lc 151:55-151:56  Type
testdata/Builtins.lc 151:55-151:66  Type
testdata/Builtins.lc 151:60-151:61  Type
testdata/Builtins.lc 151:60-151:66  Type
testdata/Builtins.lc 151:65-151:66  Type
testdata/Builtins.lc 152:1-152:10  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> a->a
testdata/Builtins.lc 152:34-152:76  Type
testdata/Builtins.lc 152:35-152:36  V4
testdata/Builtins.lc 152:35-152:38  V3->Type
testdata/Builtins.lc 152:35-152:56  Type
testdata/Builtins.lc 152:37-152:38  {a} -> a -> a->Type
testdata/Builtins.lc 152:39-152:48  Nat -> Type->Type
testdata/Builtins.lc 152:39-152:50  Type->Type
testdata/Builtins.lc 152:39-152:56  Type
testdata/Builtins.lc 152:49-152:50  V1
testdata/Builtins.lc 152:51-152:56  Type
testdata/Builtins.lc 152:61-152:66  Type
testdata/Builtins.lc 152:61-152:76  Type
testdata/Builtins.lc 152:70-152:71  Type
testdata/Builtins.lc 152:70-152:76  Type
testdata/Builtins.lc 152:75-152:76  Type
testdata/Builtins.lc 153:1-153:15  {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a -> a -> a->a
testdata/Builtins.lc 153:34-153:71  Type
testdata/Builtins.lc 153:35-153:36  V4
testdata/Builtins.lc 153:35-153:38  V3->Type
testdata/Builtins.lc 153:35-153:50  Type
testdata/Builtins.lc 153:37-153:38  {a} -> a -> a->Type
testdata/Builtins.lc 153:39-153:42  Nat -> Type->Type
testdata/Builtins.lc 153:39-153:44  Type->Type
testdata/Builtins.lc 153:39-153:50  Type
testdata/Builtins.lc 153:43-153:44  V1
testdata/Builtins.lc 153:45-153:50  Type
testdata/Builtins.lc 153:55-153:56  Type
testdata/Builtins.lc 153:55-153:71  Type
testdata/Builtins.lc 153:60-153:61  Type
testdata/Builtins.lc 153:60-153:71  Type
testdata/Builtins.lc 153:65-153:66  Type
testdata/Builtins.lc 153:65-153:71  Type
testdata/Builtins.lc 153:70-153:71  Type
testdata/Builtins.lc 154:1-154:16  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> Float -> Float -> a->a
testdata/Builtins.lc 154:34-154:85  Type
testdata/Builtins.lc 154:35-154:36  V4
testdata/Builtins.lc 154:35-154:38  V3->Type
testdata/Builtins.lc 154:35-154:56  Type
testdata/Builtins.lc 154:37-154:38  {a} -> a -> a->Type
testdata/Builtins.lc 154:39-154:48  Nat -> Type->Type
testdata/Builtins.lc 154:39-154:50  Type->Type
testdata/Builtins.lc 154:39-154:56  Type
testdata/Builtins.lc 154:49-154:50  V1
testdata/Builtins.lc 154:51-154:56  Type
testdata/Builtins.lc 154:61-154:66  Type
testdata/Builtins.lc 154:61-154:85  Type
testdata/Builtins.lc 154:70-154:75  Type
testdata/Builtins.lc 154:70-154:85  Type
testdata/Builtins.lc 154:79-154:80  Type
testdata/Builtins.lc 154:79-154:85  Type
testdata/Builtins.lc 154:84-154:85  Type
testdata/Builtins.lc 157:1-157:19  {a:Nat} -> VecScalar a Float -> VecScalar a Int
testdata/Builtins.lc 157:34-157:43  Nat -> Type->Type
testdata/Builtins.lc 157:34-157:45  Type->Type
testdata/Builtins.lc 157:34-157:51  Type
testdata/Builtins.lc 157:34-157:70  Type
testdata/Builtins.lc 157:44-157:45  V1
testdata/Builtins.lc 157:46-157:51  Type
testdata/Builtins.lc 157:55-157:64  Nat -> Type->Type
testdata/Builtins.lc 157:55-157:66  Type->Type
testdata/Builtins.lc 157:55-157:70  Type
testdata/Builtins.lc 157:65-157:66  Nat
testdata/Builtins.lc 157:67-157:70  Type
testdata/Builtins.lc 158:1-158:20  {a:Nat} -> VecScalar a Float -> VecScalar a Word
testdata/Builtins.lc 158:34-158:43  Nat -> Type->Type
testdata/Builtins.lc 158:34-158:45  Type->Type
testdata/Builtins.lc 158:34-158:51  Type
testdata/Builtins.lc 158:34-158:71  Type
testdata/Builtins.lc 158:44-158:45  V1
testdata/Builtins.lc 158:46-158:51  Type
testdata/Builtins.lc 158:55-158:64  Nat -> Type->Type
testdata/Builtins.lc 158:55-158:66  Type->Type
testdata/Builtins.lc 158:55-158:71  Type
testdata/Builtins.lc 158:65-158:66  Nat
testdata/Builtins.lc 158:67-158:71  Type
testdata/Builtins.lc 159:1-159:19  {a:Nat} -> VecScalar a Int -> VecScalar a Float
testdata/Builtins.lc 159:34-159:43  Nat -> Type->Type
testdata/Builtins.lc 159:34-159:45  Type->Type
testdata/Builtins.lc 159:34-159:49  Type
testdata/Builtins.lc 159:34-159:72  Type
testdata/Builtins.lc 159:44-159:45  V1
testdata/Builtins.lc 159:46-159:49  Type
testdata/Builtins.lc 159:55-159:64  Nat -> Type->Type
testdata/Builtins.lc 159:55-159:66  Type->Type
testdata/Builtins.lc 159:55-159:72  Type
testdata/Builtins.lc 159:65-159:66  Nat
testdata/Builtins.lc 159:67-159:72  Type
testdata/Builtins.lc 160:1-160:20  {a:Nat} -> VecScalar a Word -> VecScalar a Float
testdata/Builtins.lc 160:34-160:43  Nat -> Type->Type
testdata/Builtins.lc 160:34-160:45  Type->Type
testdata/Builtins.lc 160:34-160:50  Type
testdata/Builtins.lc 160:34-160:72  Type
testdata/Builtins.lc 160:44-160:45  V1
testdata/Builtins.lc 160:46-160:50  Type
testdata/Builtins.lc 160:55-160:64  Nat -> Type->Type
testdata/Builtins.lc 160:55-160:66  Type->Type
testdata/Builtins.lc 160:55-160:72  Type
testdata/Builtins.lc 160:65-160:66  Nat
testdata/Builtins.lc 160:67-160:72  Type
testdata/Builtins.lc 162:1-162:11  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->Float
testdata/Builtins.lc 162:34-162:71  Type
testdata/Builtins.lc 162:35-162:36  V4
testdata/Builtins.lc 162:35-162:38  V3->Type
testdata/Builtins.lc 162:35-162:56  Type
testdata/Builtins.lc 162:37-162:38  {a} -> a -> a->Type
testdata/Builtins.lc 162:39-162:48  Nat -> Type->Type
testdata/Builtins.lc 162:39-162:50  Type->Type
testdata/Builtins.lc 162:39-162:56  Type
testdata/Builtins.lc 162:49-162:50  V1
testdata/Builtins.lc 162:51-162:56  Type
testdata/Builtins.lc 162:61-162:62  Type
testdata/Builtins.lc 162:61-162:71  Type
testdata/Builtins.lc 162:66-162:71  Type
testdata/Builtins.lc 163:1-163:13  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
testdata/Builtins.lc 163:15-163:22  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->Float
testdata/Builtins.lc 163:34-163:76  Type
testdata/Builtins.lc 163:35-163:36  V4
testdata/Builtins.lc 163:35-163:38  V3->Type
testdata/Builtins.lc 163:35-163:56  Type
testdata/Builtins.lc 163:37-163:38  {a} -> a -> a->Type
testdata/Builtins.lc 163:39-163:48  Nat -> Type->Type
testdata/Builtins.lc 163:39-163:50  Type->Type
testdata/Builtins.lc 163:39-163:56  Type
testdata/Builtins.lc 163:49-163:50  V1
testdata/Builtins.lc 163:51-163:56  Type
testdata/Builtins.lc 163:61-163:62  Type
testdata/Builtins.lc 163:61-163:76  Type
testdata/Builtins.lc 163:66-163:67  Type
testdata/Builtins.lc 163:66-163:76  Type
testdata/Builtins.lc 163:71-163:76  Type
testdata/Builtins.lc 164:1-164:10  {a} -> {b : a ~ VecS Float 3} -> a -> a->a
testdata/Builtins.lc 164:34-164:72  Type
testdata/Builtins.lc 164:35-164:36  V2
testdata/Builtins.lc 164:35-164:38  V1->Type
testdata/Builtins.lc 164:35-164:56  Type
testdata/Builtins.lc 164:37-164:38  {a} -> a -> a->Type
testdata/Builtins.lc 164:39-164:48  Nat -> Type->Type
testdata/Builtins.lc 164:39-164:50  Type->Type
testdata/Builtins.lc 164:39-164:56  Type
testdata/Builtins.lc 164:49-164:50  V1
testdata/Builtins.lc 164:51-164:56  Type
testdata/Builtins.lc 164:61-164:62  Type
testdata/Builtins.lc 164:61-164:72  Type
testdata/Builtins.lc 164:66-164:67  Type
testdata/Builtins.lc 164:66-164:72  Type
testdata/Builtins.lc 164:71-164:72  Type
testdata/Builtins.lc 165:1-165:14  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 165:34-165:67  Type
testdata/Builtins.lc 165:35-165:36  V4
testdata/Builtins.lc 165:35-165:38  V3->Type
testdata/Builtins.lc 165:35-165:56  Type
testdata/Builtins.lc 165:37-165:38  {a} -> a -> a->Type
testdata/Builtins.lc 165:39-165:48  Nat -> Type->Type
testdata/Builtins.lc 165:39-165:50  Type->Type
testdata/Builtins.lc 165:39-165:56  Type
testdata/Builtins.lc 165:49-165:50  V1
testdata/Builtins.lc 165:51-165:56  Type
testdata/Builtins.lc 165:61-165:62  Type
testdata/Builtins.lc 165:61-165:67  Type
testdata/Builtins.lc 165:66-165:67  Type
testdata/Builtins.lc 166:1-166:16  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
testdata/Builtins.lc 166:18-166:29  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a -> a->a
testdata/Builtins.lc 166:34-166:77  Type
testdata/Builtins.lc 166:35-166:36  V4
testdata/Builtins.lc 166:35-166:38  V3->Type
testdata/Builtins.lc 166:35-166:56  Type
testdata/Builtins.lc 166:37-166:38  {a} -> a -> a->Type
testdata/Builtins.lc 166:39-166:48  Nat -> Type->Type
testdata/Builtins.lc 166:39-166:50  Type->Type
testdata/Builtins.lc 166:39-166:56  Type
testdata/Builtins.lc 166:49-166:50  V1
testdata/Builtins.lc 166:51-166:56  Type
testdata/Builtins.lc 166:61-166:62  Type
testdata/Builtins.lc 166:61-166:77  Type
testdata/Builtins.lc 166:66-166:67  Type
testdata/Builtins.lc 166:66-166:77  Type
testdata/Builtins.lc 166:71-166:72  Type
testdata/Builtins.lc 166:71-166:77  Type
testdata/Builtins.lc 166:76-166:77  Type
testdata/Builtins.lc 167:1-167:12  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a -> a->a
testdata/Builtins.lc 167:34-167:72  Type
testdata/Builtins.lc 167:35-167:36  V4
testdata/Builtins.lc 167:35-167:38  V3->Type
testdata/Builtins.lc 167:35-167:56  Type
testdata/Builtins.lc 167:37-167:38  {a} -> a -> a->Type
testdata/Builtins.lc 167:39-167:48  Nat -> Type->Type
testdata/Builtins.lc 167:39-167:50  Type->Type
testdata/Builtins.lc 167:39-167:56  Type
testdata/Builtins.lc 167:49-167:50  V1
testdata/Builtins.lc 167:51-167:56  Type
testdata/Builtins.lc 167:61-167:62  Type
testdata/Builtins.lc 167:61-167:72  Type
testdata/Builtins.lc 167:66-167:67  Type
testdata/Builtins.lc 167:66-167:72  Type
testdata/Builtins.lc 167:71-167:72  Type
testdata/Builtins.lc 169:1-169:14  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Mat b a c
testdata/Builtins.lc 169:34-169:37  Nat -> Nat -> Type->Type
testdata/Builtins.lc 169:34-169:39  Nat -> Type->Type
testdata/Builtins.lc 169:34-169:41  Type->Type
testdata/Builtins.lc 169:34-169:43  Type
testdata/Builtins.lc 169:34-169:56  Type
testdata/Builtins.lc 169:38-169:39  V5
testdata/Builtins.lc 169:40-169:41  V3
testdata/Builtins.lc 169:42-169:43  V1
testdata/Builtins.lc 169:47-169:50  Nat -> Nat -> Type->Type
testdata/Builtins.lc 169:47-169:52  Nat -> Type->Type
testdata/Builtins.lc 169:47-169:54  Type->Type
testdata/Builtins.lc 169:47-169:56  Type
testdata/Builtins.lc 169:51-169:52  Nat
testdata/Builtins.lc 169:53-169:54  Nat
testdata/Builtins.lc 169:55-169:56  Type
testdata/Builtins.lc 170:1-170:16  {a:Nat} -> {b} -> Mat a a b -> Float
testdata/Builtins.lc 170:34-170:37  Nat -> Nat -> Type->Type
testdata/Builtins.lc 170:34-170:39  Nat -> Type->Type
testdata/Builtins.lc 170:34-170:41  Type->Type
testdata/Builtins.lc 170:34-170:43  Type
testdata/Builtins.lc 170:34-170:52  Type
testdata/Builtins.lc 170:38-170:39  V3
testdata/Builtins.lc 170:40-170:41  Nat
testdata/Builtins.lc 170:42-170:43  V1
testdata/Builtins.lc 170:47-170:52  Type
testdata/Builtins.lc 171:1-171:12  {a:Nat} -> {b} -> Mat a a b -> Mat a a b
testdata/Builtins.lc 171:34-171:37  Nat -> Nat -> Type->Type
testdata/Builtins.lc 171:34-171:39  Nat -> Type->Type
testdata/Builtins.lc 171:34-171:41  Type->Type
testdata/Builtins.lc 171:34-171:43  Type
testdata/Builtins.lc 171:34-171:56  Type
testdata/Builtins.lc 171:38-171:39  V3
testdata/Builtins.lc 171:40-171:41  Nat
testdata/Builtins.lc 171:42-171:43  V1
testdata/Builtins.lc 171:47-171:50  Nat -> Nat -> Type->Type
testdata/Builtins.lc 171:47-171:52  Nat -> Type->Type
testdata/Builtins.lc 171:47-171:54  Type->Type
testdata/Builtins.lc 171:47-171:56  Type
testdata/Builtins.lc 171:51-171:52  Nat
testdata/Builtins.lc 171:53-171:54  Nat
testdata/Builtins.lc 171:55-171:56  Type
testdata/Builtins.lc 172:1-172:17  {a:Nat} -> {b} -> {c:Nat} -> Vec a b -> Vec c b -> Mat c a b
testdata/Builtins.lc 172:34-172:37  Nat -> Type->Type
testdata/Builtins.lc 172:34-172:39  Type->Type
testdata/Builtins.lc 172:34-172:41  Type
testdata/Builtins.lc 172:34-172:69  Type
testdata/Builtins.lc 172:38-172:39  V5
testdata/Builtins.lc 172:40-172:41  V3
testdata/Builtins.lc 172:47-172:50  Nat -> Type->Type
testdata/Builtins.lc 172:47-172:52  Type->Type
testdata/Builtins.lc 172:47-172:54  Type
testdata/Builtins.lc 172:47-172:69  Type
testdata/Builtins.lc 172:51-172:52  V2
testdata/Builtins.lc 172:53-172:54  Type
testdata/Builtins.lc 172:60-172:63  Nat -> Nat -> Type->Type
testdata/Builtins.lc 172:60-172:65  Nat -> Type->Type
testdata/Builtins.lc 172:60-172:67  Type->Type
testdata/Builtins.lc 172:60-172:69  Type
testdata/Builtins.lc 172:64-172:65  Nat
testdata/Builtins.lc 172:66-172:67  Nat
testdata/Builtins.lc 172:68-172:69  Type
testdata/Builtins.lc 173:1-173:14  {a:Nat} -> {b:Nat} -> {c} -> Mat a b c -> Vec b c -> Vec a c
testdata/Builtins.lc 173:34-173:37  Nat -> Nat -> Type->Type
testdata/Builtins.lc 173:34-173:39  Nat -> Type->Type
testdata/Builtins.lc 173:34-173:41  Type->Type
testdata/Builtins.lc 173:34-173:43  Type
testdata/Builtins.lc 173:34-173:67  Type
testdata/Builtins.lc 173:38-173:39  V5
testdata/Builtins.lc 173:40-173:41  V3
testdata/Builtins.lc 173:42-173:43  V1
testdata/Builtins.lc 173:47-173:50  Nat -> Type->Type
testdata/Builtins.lc 173:47-173:52  Type->Type
testdata/Builtins.lc 173:47-173:54  Type
testdata/Builtins.lc 173:47-173:67  Type
testdata/Builtins.lc 173:51-173:52  Nat
testdata/Builtins.lc 173:53-173:54  Type
testdata/Builtins.lc 173:60-173:63  Nat -> Type->Type
testdata/Builtins.lc 173:60-173:65  Type->Type
testdata/Builtins.lc 173:60-173:67  Type
testdata/Builtins.lc 173:64-173:65  Nat
testdata/Builtins.lc 173:66-173:67  Type
testdata/Builtins.lc 174:1-174:14  {a:Nat} -> {b} -> {c:Nat} -> Vec a b -> Mat a c b -> Vec c b
testdata/Builtins.lc 174:34-174:37  Nat -> Type->Type
testdata/Builtins.lc 174:34-174:39  Type->Type
testdata/Builtins.lc 174:34-174:41  Type
testdata/Builtins.lc 174:34-174:67  Type
testdata/Builtins.lc 174:38-174:39  V5
testdata/Builtins.lc 174:40-174:41  V3
testdata/Builtins.lc 174:47-174:50  Nat -> Nat -> Type->Type
testdata/Builtins.lc 174:47-174:52  Nat -> Type->Type
testdata/Builtins.lc 174:47-174:54  Type->Type
testdata/Builtins.lc 174:47-174:56  Type
testdata/Builtins.lc 174:47-174:67  Type
testdata/Builtins.lc 174:51-174:52  Nat
testdata/Builtins.lc 174:53-174:54  V2
testdata/Builtins.lc 174:55-174:56  Type
testdata/Builtins.lc 174:60-174:63  Nat -> Type->Type
testdata/Builtins.lc 174:60-174:65  Type->Type
testdata/Builtins.lc 174:60-174:67  Type
testdata/Builtins.lc 174:64-174:65  Nat
testdata/Builtins.lc 174:66-174:67  Type
testdata/Builtins.lc 175:1-175:14  {a:Nat} -> {b:Nat} -> {c} -> {d:Nat} -> Mat a b c -> Mat b d c -> Mat a d c
testdata/Builtins.lc 175:34-175:37  Nat -> Nat -> Type->Type
testdata/Builtins.lc 175:34-175:39  Nat -> Type->Type
testdata/Builtins.lc 175:34-175:41  Type->Type
testdata/Builtins.lc 175:34-175:43  Type
testdata/Builtins.lc 175:34-175:69  Type
testdata/Builtins.lc 175:38-175:39  V7
testdata/Builtins.lc 175:40-175:41  V5
testdata/Builtins.lc 175:42-175:43  V3
testdata/Builtins.lc 175:47-175:50  Nat -> Nat -> Type->Type
testdata/Builtins.lc 175:47-175:52  Nat -> Type->Type
testdata/Builtins.lc 175:47-175:54  Type->Type
testdata/Builtins.lc 175:47-175:56  Type
testdata/Builtins.lc 175:47-175:69  Type
testdata/Builtins.lc 175:51-175:52  Nat
testdata/Builtins.lc 175:53-175:54  V2
testdata/Builtins.lc 175:55-175:56  Type
testdata/Builtins.lc 175:60-175:63  Nat -> Nat -> Type->Type
testdata/Builtins.lc 175:60-175:65  Nat -> Type->Type
testdata/Builtins.lc 175:60-175:67  Type->Type
testdata/Builtins.lc 175:60-175:69  Type
testdata/Builtins.lc 175:64-175:65  Nat
testdata/Builtins.lc 175:66-175:67  Nat
testdata/Builtins.lc 175:68-175:69  Type
testdata/Builtins.lc 177:1-177:13  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 177:15-177:32  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 177:34-177:49  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 177:51-177:71  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 177:73-177:83  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 177:85-177:98  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
testdata/Builtins.lc 178:51-178:114  Type
testdata/Builtins.lc 178:52-178:55  Type->Type
testdata/Builtins.lc 178:52-178:57  Type
testdata/Builtins.lc 178:56-178:57  V3
testdata/Builtins.lc 178:59-178:60  V8
testdata/Builtins.lc 178:59-178:62  V7->Type
testdata/Builtins.lc 178:59-178:76  Type
testdata/Builtins.lc 178:59-178:114  Type
testdata/Builtins.lc 178:61-178:62  {a} -> a -> a->Type
testdata/Builtins.lc 178:63-178:72  Nat -> Type->Type
testdata/Builtins.lc 178:63-178:74  Type->Type
testdata/Builtins.lc 178:63-178:76  Type
testdata/Builtins.lc 178:73-178:74  V5
testdata/Builtins.lc 178:75-178:76  Type
testdata/Builtins.lc 178:78-178:79  V4
testdata/Builtins.lc 178:78-178:81  V3->Type
testdata/Builtins.lc 178:78-178:98  Type
testdata/Builtins.lc 178:78-178:114  Type
testdata/Builtins.lc 178:80-178:81  {a} -> a -> a->Type
testdata/Builtins.lc 178:82-178:91  Nat -> Type->Type
testdata/Builtins.lc 178:82-178:93  Type->Type
testdata/Builtins.lc 178:82-178:98  Type
testdata/Builtins.lc 178:92-178:93  Nat
testdata/Builtins.lc 178:94-178:98  Type
testdata/Builtins.lc 178:103-178:104  Type
testdata/Builtins.lc 178:103-178:114  Type
testdata/Builtins.lc 178:108-178:109  Type
testdata/Builtins.lc 178:108-178:114  Type
testdata/Builtins.lc 178:113-178:114  Type
testdata/Builtins.lc 179:1-179:10  {a} -> {b} -> {c : b ~ MatVecScalarElem a} -> a -> a->Bool
testdata/Builtins.lc 179:12-179:24  {a} -> {b} -> {c : b ~ MatVecScalarElem a} -> a -> a->Bool
testdata/Builtins.lc 179:47-179:89  Type
testdata/Builtins.lc 179:48-179:49  V2
testdata/Builtins.lc 179:48-179:51  V1->Type
testdata/Builtins.lc 179:48-179:70  Type
testdata/Builtins.lc 179:50-179:51  {a} -> a -> a->Type
testdata/Builtins.lc 179:52-179:68  Type->Type
testdata/Builtins.lc 179:52-179:70  Type
testdata/Builtins.lc 179:69-179:70  V2
testdata/Builtins.lc 179:75-179:76  Type
testdata/Builtins.lc 179:75-179:89  Type
testdata/Builtins.lc 179:80-179:81  Type
testdata/Builtins.lc 179:80-179:89  Type
testdata/Builtins.lc 179:85-179:89  Type
testdata/Builtins.lc 181:1-181:9  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 181:11-181:19  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 181:21-181:31  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
testdata/Builtins.lc 182:34-182:67  Type
testdata/Builtins.lc 182:35-182:36  V4
testdata/Builtins.lc 182:35-182:38  V3->Type
testdata/Builtins.lc 182:35-182:56  Type
testdata/Builtins.lc 182:37-182:38  {a} -> a -> a->Type
testdata/Builtins.lc 182:39-182:48  Nat -> Type->Type
testdata/Builtins.lc 182:39-182:50  Type->Type
testdata/Builtins.lc 182:39-182:56  Type
testdata/Builtins.lc 182:49-182:50  V1
testdata/Builtins.lc 182:51-182:56  Type
testdata/Builtins.lc 182:61-182:62  Type
testdata/Builtins.lc 182:61-182:67  Type
testdata/Builtins.lc 182:66-182:67  Type
testdata/Builtins.lc 184:1-184:11  {a:Nat} -> VecScalar a Float -> Float
testdata/Builtins.lc 184:34-184:43  Nat -> Type->Type
testdata/Builtins.lc 184:34-184:45  Type->Type
testdata/Builtins.lc 184:34-184:51  Type
testdata/Builtins.lc 184:34-184:60  Type
testdata/Builtins.lc 184:44-184:45  V1
testdata/Builtins.lc 184:46-184:51  Type
testdata/Builtins.lc 184:55-184:60  Type
testdata/Builtins.lc 185:1-185:11  {a:Nat} -> VecScalar a Float -> Vec 2 Float
testdata/Builtins.lc 185:34-185:43  Nat -> Type->Type
testdata/Builtins.lc 185:34-185:45  Type->Type
testdata/Builtins.lc 185:34-185:51  Type
testdata/Builtins.lc 185:34-185:66  Type
testdata/Builtins.lc 185:44-185:45  V1
testdata/Builtins.lc 185:46-185:51  Type
testdata/Builtins.lc 185:55-185:58  Nat -> Type->Type
testdata/Builtins.lc 185:55-185:60  Type->Type
testdata/Builtins.lc 185:55-185:66  Type
testdata/Builtins.lc 185:59-185:60  V1
testdata/Builtins.lc 185:61-185:66  Type
testdata/Builtins.lc 186:1-186:11  {a:Nat} -> VecScalar a Float -> Vec 3 Float
testdata/Builtins.lc 186:34-186:43  Nat -> Type->Type
testdata/Builtins.lc 186:34-186:45  Type->Type
testdata/Builtins.lc 186:34-186:51  Type
testdata/Builtins.lc 186:34-186:66  Type
testdata/Builtins.lc 186:44-186:45  V1
testdata/Builtins.lc 186:46-186:51  Type
testdata/Builtins.lc 186:55-186:58  Nat -> Type->Type
testdata/Builtins.lc 186:55-186:60  Type->Type
testdata/Builtins.lc 186:55-186:66  Type
testdata/Builtins.lc 186:59-186:60  V1
testdata/Builtins.lc 186:61-186:66  Type
testdata/Builtins.lc 187:1-187:11  {a:Nat} -> VecScalar a Float -> Vec 4 Float
testdata/Builtins.lc 187:34-187:43  Nat -> Type->Type
testdata/Builtins.lc 187:34-187:45  Type->Type
testdata/Builtins.lc 187:34-187:51  Type
testdata/Builtins.lc 187:34-187:66  Type
testdata/Builtins.lc 187:44-187:45  V1
testdata/Builtins.lc 187:46-187:51  Type
testdata/Builtins.lc 187:55-187:58  Nat -> Type->Type
testdata/Builtins.lc 187:55-187:60  Type->Type
testdata/Builtins.lc 187:55-187:66  Type
testdata/Builtins.lc 187:59-187:60  V1
testdata/Builtins.lc 187:61-187:66  Type
testdata/Builtins.lc 201:1-201:5  {a} -> List a -> a
testdata/Builtins.lc 201:8-201:9  V2
testdata/Builtins.lc 201:8-201:16  V0
testdata/Builtins.lc 201:15-201:16  List V2 -> V2 | V1 -> List V2 -> V2 | V3
testdata/Builtins.lc 203:6-203:8  {a} -> List a -> List a -> List a
testdata/Builtins.lc 203:14-203:16  V3
testdata/Builtins.lc 203:14-204:26  List V0 -> List V1 | V0->V1
testdata/Builtins.lc 204:14-204:15  V3
testdata/Builtins.lc 204:14-204:17  List V2 -> List V3
testdata/Builtins.lc 204:14-204:26  List V1 -> V4 | List V2 | V0 -> List V1 -> V4
testdata/Builtins.lc 204:16-204:17  {a} -> a -> List a -> List a
testdata/Builtins.lc 204:18-204:20  List V5
testdata/Builtins.lc 204:21-204:23  V7
testdata/Builtins.lc 204:24-204:26  List V6
testdata/Builtins.lc 206:1-206:6  {a} -> {b} -> (b -> a->a) -> a -> List b -> a
testdata/Builtins.lc 206:16-206:17  V5
testdata/Builtins.lc 206:16-207:39  List V1 -> V6 | V0->V1
testdata/Builtins.lc 207:21-207:22  V8
testdata/Builtins.lc 207:21-207:39  List V1 -> V6 | V0 -> List V1 -> V6
testdata/Builtins.lc 207:23-207:24  V5
testdata/Builtins.lc 207:26-207:31  V13
testdata/Builtins.lc 207:32-207:33  V9->V7
testdata/Builtins.lc 207:34-207:35  V14
testdata/Builtins.lc 207:36-207:38  List V10
testdata/Builtins.lc 209:1-209:7  {a} -> List (List a) -> List a
testdata/Builtins.lc 209:10-209:15  {a} -> {b} -> (b -> a->a) -> a -> List b -> a
testdata/Builtins.lc 209:10-209:20  List V0 -> List (List V1) -> List V2
testdata/Builtins.lc 209:10-209:23  List (List V0) -> List V1
testdata/Builtins.lc 209:16-209:20  {a} -> List a -> List a -> List a
testdata/Builtins.lc 209:21-209:23  {a} -> List a
testdata/Builtins.lc 211:1-211:4  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 211:16-211:18  {a} -> List a
testdata/Builtins.lc 211:16-212:30  List V1 -> List V1 | V0->V1
testdata/Builtins.lc 212:16-212:17  V8
testdata/Builtins.lc 212:16-212:21  List V0 -> List V1
testdata/Builtins.lc 212:16-212:30  List V2 | List V2 -> List V2 | V1 -> List V2 -> List V2
testdata/Builtins.lc 212:18-212:19  V7
testdata/Builtins.lc 212:20-212:21  {a} -> a -> List a -> List a
testdata/Builtins.lc 212:22-212:25  V8
testdata/Builtins.lc 212:26-212:27  V6->V6
testdata/Builtins.lc 212:28-212:30  List V7
testdata/Builtins.lc 214:14-214:38  Type
testdata/Builtins.lc 214:15-214:16  V3
testdata/Builtins.lc 214:20-214:23  Type
testdata/Builtins.lc 214:21-214:22  V2
testdata/Builtins.lc 214:28-214:38  Type
testdata/Builtins.lc 214:29-214:30  Type
testdata/Builtins.lc 214:35-214:38  Type
testdata/Builtins.lc 214:36-214:37  Type
testdata/Builtins.lc 215:1-215:10  {a} -> {b} -> (a -> List b) -> List a -> List b
testdata/Builtins.lc 215:17-215:23  {a} -> List (List a) -> List a
testdata/Builtins.lc 215:17-215:33  (V1 -> List V1) -> List V2 -> List V2 | List V2 | List V2 -> List V2
testdata/Builtins.lc 215:25-215:28  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 215:25-215:30  List V4 -> List (List V4)
testdata/Builtins.lc 215:25-215:32  List (List V2)
testdata/Builtins.lc 215:29-215:30  V6 -> List V6
testdata/Builtins.lc 215:31-215:32  List V3
testdata/Builtins.lc 219:6-219:11  Type | Type->Type
testdata/Builtins.lc 219:6-221:11  Type
testdata/Builtins.lc 219:6-221:13  Type
testdata/Builtins.lc 220:7-220:14  Maybe V1 | {a} -> Maybe a
testdata/Builtins.lc 221:7-221:11  Maybe V3 | Type | {a} -> a -> Maybe a
testdata/Builtins.lc 221:12-221:13  Type
testdata/Builtins.lc 224:6-224:12  Nat -> Type->Type | Type
testdata/Builtins.lc 224:19-224:22  Type
testdata/Builtins.lc 228:6-228:19  Type
testdata/Builtins.lc 228:6-233:20  Type
testdata/Builtins.lc 229:7-229:15  PrimitiveType
testdata/Builtins.lc 230:7-230:11  PrimitiveType
testdata/Builtins.lc 231:7-231:12  PrimitiveType
testdata/Builtins.lc 232:7-232:24  PrimitiveType
testdata/Builtins.lc 233:7-233:20  PrimitiveType
testdata/Builtins.lc 235:6-235:15  Type | Type -> PrimitiveType->Type
testdata/Builtins.lc 235:6-238:56  Type
testdata/Builtins.lc 235:21-235:34  Type
testdata/Builtins.lc 235:21-235:42  Type
testdata/Builtins.lc 235:38-235:42  Type
testdata/Builtins.lc 236:5-236:14  Primitive V2 'Point | {a} -> a -> Primitive a 'Point
testdata/Builtins.lc 236:5-236:53  Type
testdata/Builtins.lc 236:21-236:22  Type
testdata/Builtins.lc 236:21-236:53  Type
testdata/Builtins.lc 236:36-236:45  Type -> PrimitiveType->Type
testdata/Builtins.lc 236:36-236:47  PrimitiveType->Type
testdata/Builtins.lc 236:36-236:53  Type
testdata/Builtins.lc 236:46-236:47  Type
testdata/Builtins.lc 236:48-236:53  PrimitiveType
testdata/Builtins.lc 237:5-237:13  Primitive V4 'Line | {a} -> a -> a -> Primitive a 'Line
testdata/Builtins.lc 237:5-237:52  Type
testdata/Builtins.lc 237:21-237:22  Type
testdata/Builtins.lc 237:21-237:52  Type
testdata/Builtins.lc 237:26-237:27  Type
testdata/Builtins.lc 237:26-237:52  Type
testdata/Builtins.lc 237:36-237:45  Type -> PrimitiveType->Type
testdata/Builtins.lc 237:36-237:47  PrimitiveType->Type
testdata/Builtins.lc 237:36-237:52  Type
testdata/Builtins.lc 237:46-237:47  Type
testdata/Builtins.lc 237:48-237:52  PrimitiveType
testdata/Builtins.lc 238:5-238:17  Primitive V6 'Triangle | {a} -> a -> a -> a -> Primitive a 'Triangle
testdata/Builtins.lc 238:5-238:56  Type
testdata/Builtins.lc 238:21-238:22  Type
testdata/Builtins.lc 238:21-238:56  Type
testdata/Builtins.lc 238:26-238:27  Type
testdata/Builtins.lc 238:26-238:56  Type
testdata/Builtins.lc 238:31-238:32  Type
testdata/Builtins.lc 238:31-238:56  Type
testdata/Builtins.lc 238:36-238:45  Type -> PrimitiveType->Type
testdata/Builtins.lc 238:36-238:47  PrimitiveType->Type
testdata/Builtins.lc 238:36-238:56  Type
testdata/Builtins.lc 238:46-238:47  Type
testdata/Builtins.lc 238:48-238:56  PrimitiveType
testdata/Builtins.lc 240:1-240:13  {a} -> {b} -> {c:PrimitiveType} -> a->b -> Primitive a c -> Primitive b c
testdata/Builtins.lc 240:17-240:59  Type
testdata/Builtins.lc 240:18-240:19  V5
testdata/Builtins.lc 240:23-240:24  Type | V4
testdata/Builtins.lc 240:29-240:38  Type -> PrimitiveType->Type
testdata/Builtins.lc 240:29-240:40  PrimitiveType->Type
testdata/Builtins.lc 240:29-240:42  Type
testdata/Builtins.lc 240:29-240:59  Type
testdata/Builtins.lc 240:39-240:40  Type
testdata/Builtins.lc 240:41-240:42  V2
testdata/Builtins.lc 240:46-240:55  Type -> PrimitiveType->Type
testdata/Builtins.lc 240:46-240:57  PrimitiveType->Type
testdata/Builtins.lc 240:46-240:59  Type
testdata/Builtins.lc 240:56-240:57  Type
testdata/Builtins.lc 240:58-240:59  PrimitiveType
testdata/Builtins.lc 247:6-247:21  PrimitiveType -> Type->Type
testdata/Builtins.lc 247:29-247:38  Type -> PrimitiveType->Type
testdata/Builtins.lc 247:29-247:40  PrimitiveType->Type
testdata/Builtins.lc 247:29-247:42  Type
testdata/Builtins.lc 247:39-247:40  V1
testdata/Builtins.lc 247:41-247:42  V2
testdata/Builtins.lc 249:18-249:72  Type
testdata/Builtins.lc 249:19-249:20  V5
testdata/Builtins.lc 249:24-249:25  Type | V4
testdata/Builtins.lc 249:30-249:45  PrimitiveType -> Type->Type
testdata/Builtins.lc 249:30-249:47  Type->Type
testdata/Builtins.lc 249:30-249:49  Type
testdata/Builtins.lc 249:30-249:72  Type
testdata/Builtins.lc 249:46-249:47  V2
testdata/Builtins.lc 249:48-249:49  Type
testdata/Builtins.lc 249:53-249:68  PrimitiveType -> Type->Type
testdata/Builtins.lc 249:53-249:70  Type->Type
testdata/Builtins.lc 249:53-249:72  Type
testdata/Builtins.lc 249:69-249:70  PrimitiveType
testdata/Builtins.lc 249:71-249:72  Type
testdata/Builtins.lc 250:1-250:14  {a} -> {b} -> {c:PrimitiveType} -> a->b -> List (Primitive a c) -> List (Primitive b c)
testdata/Builtins.lc 250:19-250:22  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 250:19-250:39  List (Primitive V4 V0) -> List (Primitive V4 V1) | V2->V2 -> PrimitiveStream V1 V3 -> PrimitiveStream V2 V3
testdata/Builtins.lc 250:24-250:36  {a} -> {b} -> {c:PrimitiveType} -> a->b -> Primitive a c -> Primitive b c
testdata/Builtins.lc 250:24-250:38  Primitive V6 V0 -> Primitive V6 V1
testdata/Builtins.lc 250:37-250:38  V8->V8
testdata/Builtins.lc 252:30-252:38  Type->Type
testdata/Builtins.lc 252:40-252:41  Type
testdata/Builtins.lc 252:40-252:46  Type->Type
testdata/Builtins.lc 252:45-252:46  Type | Type->Type
testdata/Builtins.lc 257:1-257:12  {a:PrimitiveType} -> {b : List Type} -> {c : List Type} -> {d : b ~ 'map Type Type ListElem c} -> HList c -> PrimitiveStream a (HList b)
testdata/Builtins.lc 257:32-257:119  Type
testdata/Builtins.lc 257:56-257:57  V4
testdata/Builtins.lc 257:56-257:59  V3->Type
testdata/Builtins.lc 257:56-257:75  Type
testdata/Builtins.lc 257:58-257:59  {a} -> a -> a->Type
testdata/Builtins.lc 257:60-257:63  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 257:60-257:72  List Type -> List Type
testdata/Builtins.lc 257:60-257:75  List Type
testdata/Builtins.lc 257:64-257:72  Type->Type
testdata/Builtins.lc 257:73-257:75  V1
testdata/Builtins.lc 257:80-257:85  List Type -> Type
testdata/Builtins.lc 257:80-257:88  Type
testdata/Builtins.lc 257:80-257:119  Type
testdata/Builtins.lc 257:86-257:88  List Type
testdata/Builtins.lc 257:92-257:107  PrimitiveType -> Type->Type
testdata/Builtins.lc 257:92-257:109  Type->Type
testdata/Builtins.lc 257:92-257:119  Type
testdata/Builtins.lc 257:108-257:109  V5
testdata/Builtins.lc 257:111-257:116  List Type -> Type
testdata/Builtins.lc 257:111-257:118  Type
testdata/Builtins.lc 257:117-257:118  List Type
testdata/Builtins.lc 259:1-259:6  {a:PrimitiveType} -> {b} -> String -> b -> PrimitiveStream a b
testdata/Builtins.lc 259:56-259:62  Type
testdata/Builtins.lc 259:56-259:90  Type
testdata/Builtins.lc 259:66-259:67  V2
testdata/Builtins.lc 259:66-259:90  Type
testdata/Builtins.lc 259:71-259:86  PrimitiveType -> Type->Type
testdata/Builtins.lc 259:71-259:88  Type->Type
testdata/Builtins.lc 259:71-259:90  Type
testdata/Builtins.lc 259:87-259:88  V4
testdata/Builtins.lc 259:89-259:90  Type
testdata/Builtins.lc 263:6-263:14  Nat -> Type->Type
testdata/Builtins.lc 263:21-263:27  Nat -> Type->Type
testdata/Builtins.lc 263:21-263:29  Type->Type
testdata/Builtins.lc 263:21-263:56  Type
testdata/Builtins.lc 263:28-263:29  V3
testdata/Builtins.lc 263:31-263:36  Type->Type
testdata/Builtins.lc 263:31-263:55  Type
testdata/Builtins.lc 263:38-263:52  Type->Type
testdata/Builtins.lc 263:38-263:54  Type
testdata/Builtins.lc 263:53-263:54  V1
testdata/Builtins.lc 265:6-265:20  Type | Type->Type
testdata/Builtins.lc 265:6-265:39  Type
testdata/Builtins.lc 265:6-267:29  Type
testdata/Builtins.lc 265:25-265:39  SimpleFragment V3 | Type | V2 | {a} -> Vec 3 Float -> a -> SimpleFragment a
testdata/Builtins.lc 266:7-266:22  {a} -> SimpleFragment a -> VecS Float 3
testdata/Builtins.lc 266:28-266:31  Nat -> Type->Type
testdata/Builtins.lc 266:28-266:33  Type->Type
testdata/Builtins.lc 266:28-266:39  Type
testdata/Builtins.lc 266:32-266:33  V1
testdata/Builtins.lc 266:34-266:39  Type
testdata/Builtins.lc 267:7-267:21  {a} -> SimpleFragment a -> a
testdata/Builtins.lc 267:28-267:29  Type
testdata/Builtins.lc 270:6-270:20  Nat -> Type->Type
testdata/Builtins.lc 270:28-270:36  Nat -> Type->Type
testdata/Builtins.lc 270:28-270:38  Type->Type
testdata/Builtins.lc 270:28-270:40  Type
testdata/Builtins.lc 270:37-270:38  V3
testdata/Builtins.lc 270:39-270:40  V1
testdata/Builtins.lc 272:1-272:15  {a} -> {b:Nat} -> a->Float -> Fragment b a -> Fragment b a
testdata/Builtins.lc 272:19-272:63  Type
testdata/Builtins.lc 272:20-272:21  V3
testdata/Builtins.lc 272:25-272:30  Type
testdata/Builtins.lc 272:35-272:43  Nat -> Type->Type
testdata/Builtins.lc 272:35-272:45  Type->Type
testdata/Builtins.lc 272:35-272:47  Type
testdata/Builtins.lc 272:35-272:63  Type
testdata/Builtins.lc 272:44-272:45  V2
testdata/Builtins.lc 272:46-272:47  Type
testdata/Builtins.lc 272:51-272:59  Nat -> Type->Type
testdata/Builtins.lc 272:51-272:61  Type->Type
testdata/Builtins.lc 272:51-272:63  Type
testdata/Builtins.lc 272:60-272:61  Nat
testdata/Builtins.lc 272:62-272:63  Type
testdata/Builtins.lc 274:20-274:76  Type
testdata/Builtins.lc 274:21-274:22  V3
testdata/Builtins.lc 274:26-274:31  Type
testdata/Builtins.lc 274:36-274:50  Nat -> Type->Type
testdata/Builtins.lc 274:36-274:52  Type->Type
testdata/Builtins.lc 274:36-274:54  Type
testdata/Builtins.lc 274:36-274:76  Type
testdata/Builtins.lc 274:51-274:52  V2
testdata/Builtins.lc 274:53-274:54  Type
testdata/Builtins.lc 274:58-274:72  Nat -> Type->Type
testdata/Builtins.lc 274:58-274:74  Type->Type
testdata/Builtins.lc 274:58-274:76  Type
testdata/Builtins.lc 274:73-274:74  Nat
testdata/Builtins.lc 274:75-274:76  Type
testdata/Builtins.lc 275:1-275:16  {a} -> {b:Nat} -> a->Float -> List (Vector b (Maybe (SimpleFragment a))) -> List (Vector b (Maybe (SimpleFragment a)))
testdata/Builtins.lc 275:21-275:24  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 275:21-275:43  List (Vector V0 (Maybe (SimpleFragment V3))) -> List (Vector V1 (Maybe (SimpleFragment V4))) | V1->Float -> FragmentStream V1 V2 -> FragmentStream V2 V3
testdata/Builtins.lc 275:26-275:40  {a} -> {b:Nat} -> a->Float -> Fragment b a -> Fragment b a
testdata/Builtins.lc 275:26-275:42  Fragment V0 V5 -> Fragment V1 V6
testdata/Builtins.lc 275:41-275:42  V6->Float
testdata/Builtins.lc 277:1-277:15  {a} -> {b:Nat} -> a->Bool -> Fragment b a -> Fragment b a
testdata/Builtins.lc 277:19-277:62  Type
testdata/Builtins.lc 277:20-277:21  V3
testdata/Builtins.lc 277:25-277:29  Type
testdata/Builtins.lc 277:34-277:42  Nat -> Type->Type
testdata/Builtins.lc 277:34-277:44  Type->Type
testdata/Builtins.lc 277:34-277:46  Type
testdata/Builtins.lc 277:34-277:62  Type
testdata/Builtins.lc 277:43-277:44  V2
testdata/Builtins.lc 277:45-277:46  Type
testdata/Builtins.lc 277:50-277:58  Nat -> Type->Type
testdata/Builtins.lc 277:50-277:60  Type->Type
testdata/Builtins.lc 277:50-277:62  Type
testdata/Builtins.lc 277:59-277:60  Nat
testdata/Builtins.lc 277:61-277:62  Type
testdata/Builtins.lc 279:20-279:75  Type
testdata/Builtins.lc 279:21-279:22  V3
testdata/Builtins.lc 279:26-279:30  Type
testdata/Builtins.lc 279:35-279:49  Nat -> Type->Type
testdata/Builtins.lc 279:35-279:51  Type->Type
testdata/Builtins.lc 279:35-279:53  Type
testdata/Builtins.lc 279:35-279:75  Type
testdata/Builtins.lc 279:50-279:51  V2
testdata/Builtins.lc 279:52-279:53  Type
testdata/Builtins.lc 279:57-279:71  Nat -> Type->Type
testdata/Builtins.lc 279:57-279:73  Type->Type
testdata/Builtins.lc 279:57-279:75  Type
testdata/Builtins.lc 279:72-279:73  Nat
testdata/Builtins.lc 279:74-279:75  Type
testdata/Builtins.lc 280:1-280:16  {a} -> {b:Nat} -> a->Bool -> List (Vector b (Maybe (SimpleFragment a))) -> List (Vector b (Maybe (SimpleFragment a)))
testdata/Builtins.lc 280:21-280:24  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 280:21-280:43  List (Vector V0 (Maybe (SimpleFragment V3))) -> List (Vector V1 (Maybe (SimpleFragment V4))) | V1->Bool -> FragmentStream V1 V2 -> FragmentStream V2 V3
testdata/Builtins.lc 280:26-280:40  {a} -> {b:Nat} -> a->Bool -> Fragment b a -> Fragment b a
testdata/Builtins.lc 280:26-280:42  Fragment V0 V5 -> Fragment V1 V6
testdata/Builtins.lc 280:41-280:42  V6->Bool
testdata/Builtins.lc 282:1-282:12  {a} -> {b} -> {c:Nat} -> a->b -> Fragment c a -> Fragment c b
testdata/Builtins.lc 282:16-282:56  Type
testdata/Builtins.lc 282:17-282:18  V5
testdata/Builtins.lc 282:22-282:23  Type | V4
testdata/Builtins.lc 282:28-282:36  Nat -> Type->Type
testdata/Builtins.lc 282:28-282:38  Type->Type
testdata/Builtins.lc 282:28-282:40  Type
testdata/Builtins.lc 282:28-282:56  Type
testdata/Builtins.lc 282:37-282:38  V2
testdata/Builtins.lc 282:39-282:40  Type
testdata/Builtins.lc 282:44-282:52  Nat -> Type->Type
testdata/Builtins.lc 282:44-282:54  Type->Type
testdata/Builtins.lc 282:44-282:56  Type
testdata/Builtins.lc 282:53-282:54  Nat
testdata/Builtins.lc 282:55-282:56  Type
testdata/Builtins.lc 284:17-284:69  Type
testdata/Builtins.lc 284:18-284:19  V5
testdata/Builtins.lc 284:23-284:24  Type | V4
testdata/Builtins.lc 284:29-284:43  Nat -> Type->Type
testdata/Builtins.lc 284:29-284:45  Type->Type
testdata/Builtins.lc 284:29-284:47  Type
testdata/Builtins.lc 284:29-284:69  Type
testdata/Builtins.lc 284:44-284:45  V2
testdata/Builtins.lc 284:46-284:47  Type
testdata/Builtins.lc 284:51-284:65  Nat -> Type->Type
testdata/Builtins.lc 284:51-284:67  Type->Type
testdata/Builtins.lc 284:51-284:69  Type
testdata/Builtins.lc 284:66-284:67  Nat
testdata/Builtins.lc 284:68-284:69  Type
testdata/Builtins.lc 285:1-285:13  {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b)))
testdata/Builtins.lc 285:18-285:21  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 285:18-285:37  List (Vector V0 (Maybe (SimpleFragment V4))) -> List (Vector V1 (Maybe (SimpleFragment V4))) | V2->V2 -> FragmentStream V1 V3 -> FragmentStream V2 V3
testdata/Builtins.lc 285:23-285:34  {a} -> {b} -> {c:Nat} -> a->b -> Fragment c a -> Fragment c b
testdata/Builtins.lc 285:23-285:36  Fragment V0 V6 -> Fragment V1 V6
testdata/Builtins.lc 285:35-285:36  V8->V8
testdata/Builtins.lc 289:6-289:20  Type
testdata/Builtins.lc 289:6-289:56  Type
testdata/Builtins.lc 289:23-289:28  ImageSemantics | Type | Type->ImageSemantics
testdata/Builtins.lc 289:29-289:33  Type
testdata/Builtins.lc 289:36-289:43  ImageSemantics | Type | Type->ImageSemantics
testdata/Builtins.lc 289:44-289:48  Type
testdata/Builtins.lc 289:51-289:56  ImageSemantics | Type | Type->ImageSemantics
testdata/Builtins.lc 289:57-289:61  Type
testdata/Builtins.lc 291:6-291:11  Nat -> ImageSemantics->Type | Type
testdata/Builtins.lc 291:6-291:43  Type
testdata/Builtins.lc 291:18-291:21  Type
testdata/Builtins.lc 291:29-291:43  Type
testdata/Builtins.lc 293:1-293:11  {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a ('Color d)
testdata/Builtins.lc 293:45-294:55  Type
testdata/Builtins.lc 293:46-293:49  Type->Type
testdata/Builtins.lc 293:46-293:51  Type
testdata/Builtins.lc 293:50-293:51  V3
testdata/Builtins.lc 293:53-293:58  V3
testdata/Builtins.lc 293:53-293:60  V2->Type
testdata/Builtins.lc 293:53-293:74  Type
testdata/Builtins.lc 293:53-294:55  Type
testdata/Builtins.lc 293:59-293:60  {a} -> a -> a->Type
testdata/Builtins.lc 293:61-293:70  Nat -> Type->Type
testdata/Builtins.lc 293:61-293:72  Type->Type
testdata/Builtins.lc 293:61-293:74  Type
testdata/Builtins.lc 293:71-293:72  V5
testdata/Builtins.lc 293:73-293:74  Type
testdata/Builtins.lc 294:24-294:29  Type
testdata/Builtins.lc 294:24-294:55  Type
testdata/Builtins.lc 294:34-294:39  Nat -> ImageSemantics->Type
testdata/Builtins.lc 294:34-294:41  ImageSemantics->Type
testdata/Builtins.lc 294:34-294:55  Type
testdata/Builtins.lc 294:40-294:41  V7
testdata/Builtins.lc 294:43-294:48  Type->ImageSemantics
testdata/Builtins.lc 294:43-294:54  ImageSemantics
testdata/Builtins.lc 294:49-294:54  Type
testdata/Builtins.lc 295:1-295:11  {a:Nat} -> Float -> Image a ('Depth Float)
testdata/Builtins.lc 295:35-295:40  Type
testdata/Builtins.lc 295:35-295:66  Type
testdata/Builtins.lc 295:45-295:50  Nat -> ImageSemantics->Type
testdata/Builtins.lc 295:45-295:52  ImageSemantics->Type
testdata/Builtins.lc 295:45-295:66  Type
testdata/Builtins.lc 295:51-295:52  V2
testdata/Builtins.lc 295:54-295:59  Type->ImageSemantics
testdata/Builtins.lc 295:54-295:65  ImageSemantics
testdata/Builtins.lc 295:60-295:65  Type
testdata/Builtins.lc 296:1-296:13  {a:Nat} -> Int -> Image a ('Stencil Int)
testdata/Builtins.lc 296:35-296:38  Type
testdata/Builtins.lc 296:35-296:66  Type
testdata/Builtins.lc 296:45-296:50  Nat -> ImageSemantics->Type
testdata/Builtins.lc 296:45-296:52  ImageSemantics->Type
testdata/Builtins.lc 296:45-296:66  Type
testdata/Builtins.lc 296:51-296:52  V2
testdata/Builtins.lc 296:54-296:61  Type->ImageSemantics
testdata/Builtins.lc 296:54-296:65  ImageSemantics
testdata/Builtins.lc 296:62-296:65  Type
testdata/Builtins.lc 298:1-298:16  Float -> Image 1 ('Depth Float)
testdata/Builtins.lc 298:19-298:29  {a:Nat} -> Float -> Image a ('Depth Float)
testdata/Builtins.lc 298:19-298:32  Float -> Image 1 ('Depth Float)
testdata/Builtins.lc 298:31-298:32  V1
testdata/Builtins.lc 299:1-299:16  {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 ('Color c)
testdata/Builtins.lc 299:19-299:29  {a:Nat} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : d ~ VecScalar b c} -> d -> Image a ('Color d)
testdata/Builtins.lc 299:19-299:32  {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 ('Color c)
testdata/Builtins.lc 299:31-299:32  V1
testdata/Builtins.lc 306:6-306:11  Type
testdata/Builtins.lc 306:6-306:31  Type
testdata/Builtins.lc 306:14-306:16  Swizz
testdata/Builtins.lc 306:19-306:21  Swizz
testdata/Builtins.lc 306:24-306:26  Swizz
testdata/Builtins.lc 306:29-306:31  Swizz
testdata/Builtins.lc 324:16-324:48  Type
testdata/Builtins.lc 324:27-324:30  Nat -> Type->Type
testdata/Builtins.lc 324:27-324:32  Type->Type
testdata/Builtins.lc 324:27-324:34  Type
testdata/Builtins.lc 324:27-324:48  Type
testdata/Builtins.lc 324:31-324:32  V1
testdata/Builtins.lc 324:33-324:34  V2
testdata/Builtins.lc 324:38-324:43  Type
testdata/Builtins.lc 324:38-324:48  Type
testdata/Builtins.lc 324:47-324:48  Type
testdata/Builtins.lc 325:1-325:12  {a} -> {b:Nat} -> Vec b a -> Swizz->a
testdata/Builtins.lc 325:14-325:16  Vec V4 V5
testdata/Builtins.lc 325:14-333:32  Swizz->V3 | V3 | Vec V0 V1 -> Swizz->V3
testdata/Builtins.lc 325:22-325:24  Swizz
testdata/Builtins.lc 325:22-326:28  V1 -> V2->V2 | V2 | V2->V2
testdata/Builtins.lc 325:22-329:30  (V0 -> V1 -> V2 -> V3->V4) -> {f:Nat} -> VecS V2 f -> V3
testdata/Builtins.lc 325:22-333:32  {a:Nat} -> VecS V1 a -> V2
testdata/Builtins.lc 325:27-325:28  V4
testdata/Builtins.lc 325:27-326:28  V3 -> V4 -> Swizz->V6
testdata/Builtins.lc 326:27-326:28  V3
testdata/Builtins.lc 327:24-327:26  Swizz
testdata/Builtins.lc 327:24-329:30  V0 -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
testdata/Builtins.lc 327:29-327:30  V4
testdata/Builtins.lc 327:29-328:30  V3 -> V4 -> Swizz->V6
testdata/Builtins.lc 327:29-329:30  V3 -> Swizz->V5
testdata/Builtins.lc 328:29-328:30  V3
testdata/Builtins.lc 329:29-329:30  V3
testdata/Builtins.lc 330:26-330:28  Swizz
testdata/Builtins.lc 330:26-333:32  V0 -> V1 -> V2 -> V3->V4 | V1 -> V2 -> V3->V4 | V2 -> V3->V4 | V3->V4 | V4
testdata/Builtins.lc 330:31-330:32  V5
testdata/Builtins.lc 330:31-331:32  V4 -> V5 -> Swizz->V7
testdata/Builtins.lc 330:31-332:32  V4 -> Swizz->V6
testdata/Builtins.lc 330:31-333:32  Swizz->V5
testdata/Builtins.lc 331:31-331:32  V4
testdata/Builtins.lc 332:31-332:32  V4
testdata/Builtins.lc 333:31-333:32  V4
testdata/Builtins.lc 336:28-336:31  Nat -> Type->Type
testdata/Builtins.lc 336:28-336:33  Type->Type
testdata/Builtins.lc 336:28-336:35  Type
testdata/Builtins.lc 336:28-336:43  Type
testdata/Builtins.lc 336:32-336:33  V1
testdata/Builtins.lc 336:34-336:35  V2
testdata/Builtins.lc 336:39-336:43  Type
testdata/Builtins.lc 337:1-337:11  {a} -> {b:Nat} -> Vec b a -> Bool
testdata/Builtins.lc 337:13-337:15  Vec V3 V4
testdata/Builtins.lc 337:13-339:31  Bool | Vec V0 V1 -> Bool
testdata/Builtins.lc 337:23-337:27  Bool | V1 -> V2->V2 | V2->V2
testdata/Builtins.lc 337:23-338:29  (V0 -> V1 -> V2 -> V3->Bool) -> {f:Nat} -> VecS V2 f -> Bool
testdata/Builtins.lc 337:23-339:31  {a:Nat} -> VecS V1 a -> Bool
testdata/Builtins.lc 338:25-338:29  Bool | V0 -> V1 -> V2->Bool | V1 -> V2->Bool | V2->Bool
testdata/Builtins.lc 339:27-339:31  Bool | V0 -> V1 -> V2 -> V3->Bool | V1 -> V2 -> V3->Bool | V2 -> V3->Bool | V3->Bool
testdata/Builtins.lc 341:16-341:71  Type
testdata/Builtins.lc 341:27-341:71  Type
testdata/Builtins.lc 341:38-341:41  Nat -> Type->Type
testdata/Builtins.lc 341:38-341:43  Type->Type
testdata/Builtins.lc 341:38-341:45  Type
testdata/Builtins.lc 341:38-341:71  Type
testdata/Builtins.lc 341:42-341:43  V3
testdata/Builtins.lc 341:44-341:45  V4
testdata/Builtins.lc 341:49-341:52  Nat -> Type->Type
testdata/Builtins.lc 341:49-341:54  Type->Type
testdata/Builtins.lc 341:49-341:60  Type
testdata/Builtins.lc 341:49-341:71  Type
testdata/Builtins.lc 341:53-341:54  V2
testdata/Builtins.lc 341:55-341:60  Type
testdata/Builtins.lc 341:64-341:67  Nat -> Type->Type
testdata/Builtins.lc 341:64-341:69  Type->Type
testdata/Builtins.lc 341:64-341:71  Type
testdata/Builtins.lc 341:68-341:69  Nat
testdata/Builtins.lc 341:70-341:71  Type
testdata/Builtins.lc 342:1-342:12  {a} -> {b:Nat} -> {c:Nat} -> Vec b a -> Vec c Swizz -> VecS a c
testdata/Builtins.lc 342:19-342:29  {a} -> {b:Nat} -> Vec b a -> Bool
testdata/Builtins.lc 342:19-342:31  Bool
testdata/Builtins.lc 342:19-342:58  Vec V1 Swizz -> Vec V2 V4 | Vec V1 V2 -> Vec V1 Swizz -> Vec V2 V4 | VecS V4 V2
testdata/Builtins.lc 342:30-342:31  Vec V5 V6
testdata/Builtins.lc 342:34-342:40  {a} -> {b} -> {c:Nat} -> a->b -> VecS a c -> VecS b c
testdata/Builtins.lc 342:34-342:56  VecS Swizz V0 -> VecS V7 V1
testdata/Builtins.lc 342:34-342:58  VecS V4 V2
testdata/Builtins.lc 342:42-342:53  {a} -> {b:Nat} -> Vec b a -> Swizz->a
testdata/Builtins.lc 342:42-342:55  Swizz->V9
testdata/Builtins.lc 342:54-342:55  Vec V9 V10
testdata/Builtins.lc 342:57-342:58  Vec V3 Swizz
testdata/Builtins.lc 346:6-346:20  Type
testdata/Builtins.lc 346:6-361:23  Type
testdata/Builtins.lc 347:7-347:12  BlendingFactor
testdata/Builtins.lc 348:7-348:10  BlendingFactor
testdata/Builtins.lc 349:7-349:15  BlendingFactor
testdata/Builtins.lc 350:7-350:23  BlendingFactor
testdata/Builtins.lc 351:7-351:15  BlendingFactor
testdata/Builtins.lc 352:7-352:23  BlendingFactor
testdata/Builtins.lc 353:7-353:15  BlendingFactor
testdata/Builtins.lc 354:7-354:23  BlendingFactor
testdata/Builtins.lc 355:7-355:15  BlendingFactor
testdata/Builtins.lc 356:7-356:23  BlendingFactor
testdata/Builtins.lc 357:7-357:20  BlendingFactor
testdata/Builtins.lc 358:7-358:28  BlendingFactor
testdata/Builtins.lc 359:7-359:20  BlendingFactor
testdata/Builtins.lc 360:7-360:28  BlendingFactor
testdata/Builtins.lc 361:7-361:23  BlendingFactor
testdata/Builtins.lc 363:6-363:19  Type
testdata/Builtins.lc 363:6-368:10  Type
testdata/Builtins.lc 364:7-364:14  BlendEquation
testdata/Builtins.lc 365:7-365:19  BlendEquation
testdata/Builtins.lc 366:7-366:26  BlendEquation
testdata/Builtins.lc 367:7-367:10  BlendEquation
testdata/Builtins.lc 368:7-368:10  BlendEquation
testdata/Builtins.lc 370:6-370:20  Type
testdata/Builtins.lc 370:6-386:10  Type
testdata/Builtins.lc 371:7-371:12  LogicOperation
testdata/Builtins.lc 372:7-372:10  LogicOperation
testdata/Builtins.lc 373:7-373:17  LogicOperation
testdata/Builtins.lc 374:7-374:11  LogicOperation
testdata/Builtins.lc 375:7-375:18  LogicOperation
testdata/Builtins.lc 376:7-376:11  LogicOperation
testdata/Builtins.lc 377:7-377:10  LogicOperation
testdata/Builtins.lc 378:7-378:9  LogicOperation
testdata/Builtins.lc 379:7-379:10  LogicOperation
testdata/Builtins.lc 380:7-380:12  LogicOperation
testdata/Builtins.lc 381:7-381:13  LogicOperation
testdata/Builtins.lc 382:7-382:16  LogicOperation
testdata/Builtins.lc 383:7-383:19  LogicOperation
testdata/Builtins.lc 384:7-384:17  LogicOperation
testdata/Builtins.lc 385:7-385:11  LogicOperation
testdata/Builtins.lc 386:7-386:10  LogicOperation
testdata/Builtins.lc 388:6-388:22  Type
testdata/Builtins.lc 388:6-396:15  Type
testdata/Builtins.lc 389:7-389:13  StencilOperation
testdata/Builtins.lc 390:7-390:13  StencilOperation
testdata/Builtins.lc 391:7-391:16  StencilOperation
testdata/Builtins.lc 392:7-392:13  StencilOperation
testdata/Builtins.lc 393:7-393:17  StencilOperation
testdata/Builtins.lc 394:7-394:13  StencilOperation
testdata/Builtins.lc 395:7-395:17  StencilOperation
testdata/Builtins.lc 396:7-396:15  StencilOperation
testdata/Builtins.lc 398:6-398:24  Type
testdata/Builtins.lc 398:6-406:13  Type
testdata/Builtins.lc 399:7-399:12  ComparisonFunction
testdata/Builtins.lc 400:7-400:11  ComparisonFunction
testdata/Builtins.lc 401:7-401:12  ComparisonFunction
testdata/Builtins.lc 402:7-402:13  ComparisonFunction
testdata/Builtins.lc 403:7-403:14  ComparisonFunction
testdata/Builtins.lc 404:7-404:15  ComparisonFunction
testdata/Builtins.lc 405:7-405:13  ComparisonFunction
testdata/Builtins.lc 406:7-406:13  ComparisonFunction
testdata/Builtins.lc 408:6-408:21  Type
testdata/Builtins.lc 408:6-410:18  Type
testdata/Builtins.lc 409:7-409:17  ProvokingVertex
testdata/Builtins.lc 410:7-410:18  ProvokingVertex
testdata/Builtins.lc 412:6-412:14  Type
testdata/Builtins.lc 412:6-415:15  Type
testdata/Builtins.lc 413:7-413:16  CullMode
testdata/Builtins.lc 414:7-414:15  CullMode
testdata/Builtins.lc 415:7-415:15  CullMode
testdata/Builtins.lc 417:6-417:15  Type | Type->Type
testdata/Builtins.lc 417:6-418:22  Type
testdata/Builtins.lc 417:6-419:23  Type
testdata/Builtins.lc 417:6-419:36  Type
testdata/Builtins.lc 418:7-418:16  PointSize V2 | Type | {a} -> Float -> PointSize a
testdata/Builtins.lc 418:17-418:22  Type
testdata/Builtins.lc 419:7-419:23  PointSize V3 | Type | {a} -> a->Float -> PointSize a
testdata/Builtins.lc 419:25-419:26  Type
testdata/Builtins.lc 419:30-419:35  Type
testdata/Builtins.lc 421:6-421:17  Type | Type->Type
testdata/Builtins.lc 421:6-423:33  Type
testdata/Builtins.lc 421:6-424:18  Type
testdata/Builtins.lc 421:6-424:24  Type
testdata/Builtins.lc 422:7-422:18  PolygonMode V1 | {a} -> PolygonMode a
testdata/Builtins.lc 423:7-423:19  PolygonMode V3 | Type | {a} -> PointSize a -> PolygonMode a
testdata/Builtins.lc 423:21-423:30  Type->Type
testdata/Builtins.lc 423:21-423:32  Type
testdata/Builtins.lc 423:31-423:32  Type
testdata/Builtins.lc 424:7-424:18  PolygonMode V4 | Type | {a} -> Float -> PolygonMode a
testdata/Builtins.lc 424:19-424:24  Type
testdata/Builtins.lc 426:6-426:19  Type
testdata/Builtins.lc 426:6-428:13  Type
testdata/Builtins.lc 426:6-428:25  Type
testdata/Builtins.lc 427:7-427:15  PolygonOffset
testdata/Builtins.lc 428:7-428:13  Float -> Float->PolygonOffset | PolygonOffset | Type
testdata/Builtins.lc 428:14-428:19  Type
testdata/Builtins.lc 428:20-428:25  Type
testdata/Builtins.lc 430:6-430:28  Type
testdata/Builtins.lc 430:6-432:16  Type
testdata/Builtins.lc 431:7-431:16  PointSpriteCoordOrigin
testdata/Builtins.lc 432:7-432:16  PointSpriteCoordOrigin
testdata/Builtins.lc 435:1-435:12  () -> Vec 2 Float -> Vec 4 Float
testdata/Builtins.lc 435:22-435:25  Nat -> Type->Type
testdata/Builtins.lc 435:22-435:27  Type->Type
testdata/Builtins.lc 435:22-435:33  Type
testdata/Builtins.lc 435:22-435:48  Type
testdata/Builtins.lc 435:26-435:27  V1
testdata/Builtins.lc 435:28-435:33  Type
testdata/Builtins.lc 435:37-435:40  Nat -> Type->Type
testdata/Builtins.lc 435:37-435:42  Type->Type
testdata/Builtins.lc 435:37-435:48  Type
testdata/Builtins.lc 435:41-435:42  V1
testdata/Builtins.lc 435:43-435:48  Type
testdata/Builtins.lc 438:1-438:8  {a} -> String->a
testdata/Builtins.lc 438:14-438:20  Type
testdata/Builtins.lc 438:14-438:25  Type
testdata/Builtins.lc 438:24-438:25  Type | V2
testdata/Builtins.lc 439:1-439:10  {a} -> String->a
testdata/Builtins.lc 439:14-439:20  Type
testdata/Builtins.lc 439:14-439:25  Type
testdata/Builtins.lc 439:24-439:25  Type | V2
testdata/Builtins.lc 441:6-441:19  Type | Type -> PrimitiveType->Type
testdata/Builtins.lc 441:6-444:111  Type
testdata/Builtins.lc 441:25-441:38  Type
testdata/Builtins.lc 441:25-441:46  Type
testdata/Builtins.lc 441:42-441:46  Type
testdata/Builtins.lc 442:3-442:14  RasterContext V5 'Triangle | {a} -> CullMode -> PolygonMode a -> PolygonOffset -> ProvokingVertex -> RasterContext a 'Triangle
testdata/Builtins.lc 442:3-442:115  Type
testdata/Builtins.lc 442:26-442:34  Type
testdata/Builtins.lc 442:26-442:115  Type
testdata/Builtins.lc 442:38-442:49  Type->Type
testdata/Builtins.lc 442:38-442:51  Type
testdata/Builtins.lc 442:38-442:115  Type
testdata/Builtins.lc 442:50-442:51  Type
testdata/Builtins.lc 442:55-442:68  Type
testdata/Builtins.lc 442:55-442:115  Type
testdata/Builtins.lc 442:72-442:87  Type
testdata/Builtins.lc 442:72-442:115  Type
testdata/Builtins.lc 442:91-442:104  Type -> PrimitiveType->Type
testdata/Builtins.lc 442:91-442:106  PrimitiveType->Type
testdata/Builtins.lc 442:91-442:115  Type
testdata/Builtins.lc 442:105-442:106  Type
testdata/Builtins.lc 442:107-442:115  PrimitiveType
testdata/Builtins.lc 443:3-443:11  RasterContext V5 'Point | {a} -> PointSize a -> Float -> PointSpriteCoordOrigin -> RasterContext a 'Point
testdata/Builtins.lc 443:3-443:112  Type
testdata/Builtins.lc 443:26-443:35  Type->Type
testdata/Builtins.lc 443:26-443:37  Type
testdata/Builtins.lc 443:26-443:112  Type
testdata/Builtins.lc 443:36-443:37  Type
testdata/Builtins.lc 443:41-443:46  Type
testdata/Builtins.lc 443:41-443:112  Type
testdata/Builtins.lc 443:50-443:72  Type
testdata/Builtins.lc 443:50-443:112  Type
testdata/Builtins.lc 443:91-443:104  Type -> PrimitiveType->Type
testdata/Builtins.lc 443:91-443:106  PrimitiveType->Type
testdata/Builtins.lc 443:91-443:112  Type
testdata/Builtins.lc 443:105-443:106  Type
testdata/Builtins.lc 443:107-443:112  PrimitiveType
testdata/Builtins.lc 444:3-444:10  RasterContext V5 'Line | {a} -> Float -> ProvokingVertex -> RasterContext a 'Line
testdata/Builtins.lc 444:3-444:111  Type
testdata/Builtins.lc 444:26-444:31  Type
testdata/Builtins.lc 444:26-444:111  Type
testdata/Builtins.lc 444:35-444:50  Type
testdata/Builtins.lc 444:35-444:111  Type
testdata/Builtins.lc 444:91-444:104  Type -> PrimitiveType->Type
testdata/Builtins.lc 444:91-444:106  PrimitiveType->Type
testdata/Builtins.lc 444:91-444:111  Type
testdata/Builtins.lc 444:105-444:106  Type
testdata/Builtins.lc 444:107-444:111  PrimitiveType
testdata/Builtins.lc 446:6-446:14  Type | Type->Type
testdata/Builtins.lc 446:6-451:74  Type
testdata/Builtins.lc 446:18-446:22  Type
testdata/Builtins.lc 446:26-446:30  Type
testdata/Builtins.lc 447:3-447:13  Blending V0 | {a} -> Blending a
testdata/Builtins.lc 447:3-447:70  Type
testdata/Builtins.lc 447:60-447:68  Type->Type
testdata/Builtins.lc 447:60-447:70  Type
testdata/Builtins.lc 447:69-447:70  Type | V1
testdata/Builtins.lc 448:3-448:15  Blending V2 | {a} -> {b : Integral a} -> LogicOperation -> Blending a
testdata/Builtins.lc 448:3-448:70  Type
testdata/Builtins.lc 448:26-448:70  Type
testdata/Builtins.lc 448:27-448:35  Type->Type
testdata/Builtins.lc 448:27-448:37  Type
testdata/Builtins.lc 448:36-448:37  V1
testdata/Builtins.lc 448:42-448:56  Type
testdata/Builtins.lc 448:42-448:70  Type
testdata/Builtins.lc 448:60-448:68  Type->Type
testdata/Builtins.lc 448:60-448:70  Type
testdata/Builtins.lc 448:69-448:70  Type
testdata/Builtins.lc 449:3-449:8  (BlendEquation, BlendEquation) -> ((BlendingFactor, BlendingFactor), (BlendingFactor, BlendingFactor)) -> Vec 4 Float -> Blending Float | Blending Float
testdata/Builtins.lc 449:3-451:74  Type
testdata/Builtins.lc 449:27-449:40  Type
testdata/Builtins.lc 449:27-449:55  List Type
testdata/Builtins.lc 449:42-449:55  List Type | Type
testdata/Builtins.lc 450:29-451:74  Type
testdata/Builtins.lc 450:30-450:62  Type
testdata/Builtins.lc 450:30-450:96  List Type
testdata/Builtins.lc 450:31-450:45  Type
testdata/Builtins.lc 450:31-450:61  List Type
testdata/Builtins.lc 450:47-450:61  List Type | Type
testdata/Builtins.lc 450:64-450:96  List Type | Type
testdata/Builtins.lc 450:65-450:79  Type
testdata/Builtins.lc 450:65-450:95  List Type
testdata/Builtins.lc 450:81-450:95  List Type | Type
testdata/Builtins.lc 451:29-451:32  Nat -> Type->Type
testdata/Builtins.lc 451:29-451:34  Type->Type
testdata/Builtins.lc 451:29-451:40  Type
testdata/Builtins.lc 451:29-451:74  Type
testdata/Builtins.lc 451:33-451:34  V1
testdata/Builtins.lc 451:35-451:40  Type
testdata/Builtins.lc 451:60-451:68  Type->Type
testdata/Builtins.lc 451:60-451:74  Type
testdata/Builtins.lc 451:69-451:74  Type
testdata/Builtins.lc 453:6-453:18  Type
testdata/Builtins.lc 454:6-454:16  Type
testdata/Builtins.lc 455:6-455:11  Type
testdata/Builtins.lc 457:6-457:23  ImageSemantics->Type | Type
testdata/Builtins.lc 457:6-460:104  Type
testdata/Builtins.lc 457:27-457:41  Type
testdata/Builtins.lc 457:45-457:49  Type
testdata/Builtins.lc 458:3-458:10  FragmentOperation ('Color (VecScalar V3 V4)) | {a} -> {b:Nat} -> {c : Num a} -> Blending a -> VecScalar b Bool -> FragmentOperation ('Color (VecScalar b a))
testdata/Builtins.lc 458:3-458:112  Type
testdata/Builtins.lc 458:26-458:29  Type->Type
testdata/Builtins.lc 458:26-458:31  Type
testdata/Builtins.lc 458:26-458:112  Type
testdata/Builtins.lc 458:30-458:31  V3
testdata/Builtins.lc 458:35-458:43  Type->Type
testdata/Builtins.lc 458:35-458:45  Type
testdata/Builtins.lc 458:35-458:112  Type
testdata/Builtins.lc 458:44-458:45  Type
testdata/Builtins.lc 458:49-458:58  Nat -> Type->Type
testdata/Builtins.lc 458:49-458:60  Type->Type
testdata/Builtins.lc 458:49-458:65  Type
testdata/Builtins.lc 458:49-458:112  Type
testdata/Builtins.lc 458:59-458:60  V3
testdata/Builtins.lc 458:61-458:65  Type
testdata/Builtins.lc 458:71-458:88  ImageSemantics->Type
testdata/Builtins.lc 458:71-458:112  Type
testdata/Builtins.lc 458:90-458:95  Type->ImageSemantics
testdata/Builtins.lc 458:90-458:111  ImageSemantics
testdata/Builtins.lc 458:97-458:106  Nat -> Type->Type
testdata/Builtins.lc 458:97-458:108  Type->Type
testdata/Builtins.lc 458:97-458:110  Type
testdata/Builtins.lc 458:107-458:108  Nat
testdata/Builtins.lc 458:109-458:110  Type
testdata/Builtins.lc 459:3-459:10  ComparisonFunction -> Bool -> FragmentOperation ('Depth Float) | FragmentOperation ('Depth Float)
testdata/Builtins.lc 459:3-459:102  Type
testdata/Builtins.lc 459:26-459:44  Type
testdata/Builtins.lc 459:48-459:52  Type
testdata/Builtins.lc 459:48-459:102  Type
testdata/Builtins.lc 459:71-459:88  ImageSemantics->Type
testdata/Builtins.lc 459:71-459:102  Type
testdata/Builtins.lc 459:90-459:95  Type->ImageSemantics
testdata/Builtins.lc 459:90-459:101  ImageSemantics
testdata/Builtins.lc 459:96-459:101  Type
testdata/Builtins.lc 460:3-460:12  FragmentOperation ('Stencil Int32) | StencilTests -> StencilOps -> StencilOps -> FragmentOperation ('Stencil Int32)
testdata/Builtins.lc 460:3-460:104  Type
testdata/Builtins.lc 460:26-460:38  Type
testdata/Builtins.lc 460:42-460:52  Type
testdata/Builtins.lc 460:42-460:104  Type
testdata/Builtins.lc 460:56-460:66  Type
testdata/Builtins.lc 460:56-460:104  Type
testdata/Builtins.lc 460:71-460:88  ImageSemantics->Type
testdata/Builtins.lc 460:71-460:104  Type
testdata/Builtins.lc 460:90-460:97  Type->ImageSemantics
testdata/Builtins.lc 460:90-460:103  ImageSemantics
testdata/Builtins.lc 460:98-460:103  Type
testdata/Builtins.lc 462:6-462:18  Type | Type->Type
testdata/Builtins.lc 462:6-465:7  Type
testdata/Builtins.lc 463:3-463:9  Interpolated V2 | Type | {a} -> {b : Floating a} -> Interpolated a
testdata/Builtins.lc 463:11-463:24  Interpolated V3 | Type | {a} -> {b : Floating a} -> Interpolated a
testdata/Builtins.lc 464:26-464:56  Type
testdata/Builtins.lc 464:27-464:35  Type->Type
testdata/Builtins.lc 464:27-464:37  Type
testdata/Builtins.lc 464:36-464:37  Type
testdata/Builtins.lc 464:42-464:54  Type->Type
testdata/Builtins.lc 464:42-464:56  Type
testdata/Builtins.lc 464:55-464:56  Type
testdata/Builtins.lc 465:3-465:7  Interpolated V3 | {a} -> Interpolated a
testdata/Builtins.lc 465:42-465:54  Type->Type
testdata/Builtins.lc 465:42-465:56  Type
testdata/Builtins.lc 465:55-465:56  Type
testdata/Builtins.lc 467:1-467:19  {a : List Type} -> {b : List Type} -> {c : List Type} -> {d:PrimitiveType} -> {e : 'map Type Type Interpolated a ~ b} -> {f : c ~ 'Cons (Vec 4 Float) a} -> HList b -> RasterContext (HList c) d -> Primitive (HList c) d -> FragmentStream 1 (HList a)
testdata/Builtins.lc 468:8-473:34  Type
testdata/Builtins.lc 468:10-468:13  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 468:10-468:26  List Type -> List Type
testdata/Builtins.lc 468:10-468:28  List Type
testdata/Builtins.lc 468:10-468:30  List Type -> Type
testdata/Builtins.lc 468:10-468:44  Type
testdata/Builtins.lc 468:14-468:26  Type->Type
testdata/Builtins.lc 468:27-468:28  V7
testdata/Builtins.lc 468:29-468:30  {a} -> a -> a->Type
testdata/Builtins.lc 468:31-468:44  V5
testdata/Builtins.lc 469:10-469:11  V5
testdata/Builtins.lc 469:10-469:13  V4->Type
testdata/Builtins.lc 469:10-469:35  Type
testdata/Builtins.lc 469:10-473:34  Type
testdata/Builtins.lc 469:12-469:13  {a} -> a -> a->Type
testdata/Builtins.lc 469:14-469:19  {a} -> a -> List a -> List a
testdata/Builtins.lc 469:14-469:33  List Type -> List Type
testdata/Builtins.lc 469:14-469:35  List Type
testdata/Builtins.lc 469:21-469:24  Nat -> Type->Type
testdata/Builtins.lc 469:21-469:26  Type->Type
testdata/Builtins.lc 469:21-469:32  Type
testdata/Builtins.lc 469:25-469:26  V1
testdata/Builtins.lc 469:27-469:32  Type
testdata/Builtins.lc 469:34-469:35  List Type
testdata/Builtins.lc 470:8-470:13  List Type -> Type
testdata/Builtins.lc 470:8-470:27  Type
testdata/Builtins.lc 470:8-473:34  Type
testdata/Builtins.lc 470:14-470:27  List Type
testdata/Builtins.lc 471:8-471:21  Type -> PrimitiveType->Type
testdata/Builtins.lc 471:8-471:31  PrimitiveType->Type
testdata/Builtins.lc 471:8-471:33  Type
testdata/Builtins.lc 471:8-473:34  Type
testdata/Builtins.lc 471:23-471:28  List Type -> Type
testdata/Builtins.lc 471:23-471:30  Type
testdata/Builtins.lc 471:29-471:30  List Type
testdata/Builtins.lc 471:32-471:33  V4
testdata/Builtins.lc 472:8-472:17  Type -> PrimitiveType->Type
testdata/Builtins.lc 472:8-472:27  PrimitiveType->Type
testdata/Builtins.lc 472:8-472:29  Type
testdata/Builtins.lc 472:8-473:34  Type
testdata/Builtins.lc 472:19-472:24  List Type -> Type
testdata/Builtins.lc 472:19-472:26  Type
testdata/Builtins.lc 472:25-472:26  List Type
testdata/Builtins.lc 472:28-472:29  PrimitiveType
testdata/Builtins.lc 473:8-473:22  Nat -> Type->Type
testdata/Builtins.lc 473:8-473:24  Type->Type
testdata/Builtins.lc 473:8-473:34  Type
testdata/Builtins.lc 473:23-473:24  V1
testdata/Builtins.lc 473:26-473:31  List Type -> Type
testdata/Builtins.lc 473:26-473:33  Type
testdata/Builtins.lc 473:32-473:33  List Type
testdata/Builtins.lc 475:1-475:20  {a : List Type} -> {b:PrimitiveType} -> RasterContext (HList ('Cons (Vec 4 Float) a)) b -> HList ('map Type Type Interpolated a) -> List (Primitive (HList ('Cons (Vec 4 Float) a)) b) -> List (Vector 1 (Maybe (SimpleFragment (HList a))))
testdata/Builtins.lc 475:32-475:38  {a} -> List (List a) -> List a
testdata/Builtins.lc 475:32-475:74  List (Vector 1 (Maybe (SimpleFragment (HList V1))))
testdata/Builtins.lc 475:40-475:43  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 475:40-475:71  List (Primitive (HList ('Cons (Vec 4 Float) V1)) V0) -> List (List (Fragment 1 (HList V2)))
testdata/Builtins.lc 475:40-475:73  List (List (Fragment 1 (HList V1)))
testdata/Builtins.lc 475:45-475:63  {a : List Type} -> {b : List Type} -> {c : List Type} -> {d:PrimitiveType} -> {e : 'map Type Type Interpolated a ~ b} -> {f : c ~ 'Cons (Vec 4 Float) a} -> HList b -> RasterContext (HList c) d -> Primitive (HList c) d -> FragmentStream 1 (HList a)
testdata/Builtins.lc 475:45-475:66  RasterContext (HList ('Cons (Vec 4 Float) V1)) V0 -> Primitive (HList ('Cons (Vec 4 Float) V2)) V1 -> FragmentStream 1 (HList V3)
testdata/Builtins.lc 475:45-475:70  Primitive (HList ('Cons (Vec 4 Float) V1)) V0 -> FragmentStream 1 (HList V2)
testdata/Builtins.lc 475:64-475:66  V8
testdata/Builtins.lc 475:67-475:70  V7
testdata/Builtins.lc 475:72-475:73  V3
testdata/Builtins.lc 477:26-477:29  Type
testdata/Builtins.lc 477:36-477:43  Type->Nat
testdata/Builtins.lc 477:45-477:50  Type
testdata/Builtins.lc 477:45-477:59  Nat->Nat | Type->Nat
testdata/Builtins.lc 477:58-477:59  ImageSemantics->Nat | Nat | Nat -> ImageSemantics->Nat
testdata/Builtins.lc 479:12-479:23  Type
testdata/Builtins.lc 479:12-482:50  V0->V1 | {a} -> List a -> Type
testdata/Builtins.lc 479:13-479:14  V1
testdata/Builtins.lc 479:19-479:23  Type
testdata/Builtins.lc 480:1-480:8  {a} -> List a -> Type
testdata/Builtins.lc 480:14-480:19  Type
testdata/Builtins.lc 480:14-482:50  List V0 -> Type | Type
testdata/Builtins.lc 481:15-481:20  Type
testdata/Builtins.lc 481:15-482:50  List V1 -> Type | List V2 -> Type | Type | V0 -> List V1 -> Type
testdata/Builtins.lc 482:22-482:25  Type -> Type->Type
testdata/Builtins.lc 482:22-482:33  Type->Type
testdata/Builtins.lc 482:22-482:50  List V1 -> Type | Type | V0 -> List V1 -> Type
testdata/Builtins.lc 482:27-482:28  V6
testdata/Builtins.lc 482:27-482:30  V5->Type
testdata/Builtins.lc 482:27-482:32  Type
testdata/Builtins.lc 482:29-482:30  {a} -> a -> a->Type
testdata/Builtins.lc 482:31-482:32  V2
testdata/Builtins.lc 482:35-482:42  {a} -> List a -> Type
testdata/Builtins.lc 482:35-482:49  Type
testdata/Builtins.lc 482:44-482:45  V6
testdata/Builtins.lc 482:44-482:46  List V5 -> List V6
testdata/Builtins.lc 482:44-482:48  List V4
testdata/Builtins.lc 482:45-482:46  {a} -> a -> List a -> List a
testdata/Builtins.lc 482:46-482:48  List V4
testdata/Builtins.lc 484:1-484:16  List Type -> Type
testdata/Builtins.lc 484:21-484:28  {a} -> List a -> Type
testdata/Builtins.lc 484:21-484:45  Type
testdata/Builtins.lc 484:30-484:33  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 484:30-484:42  List Type -> List Nat
testdata/Builtins.lc 484:30-484:44  List Nat
testdata/Builtins.lc 484:34-484:42  Type->Nat
testdata/Builtins.lc 484:43-484:44  V1
testdata/Builtins.lc 496:6-496:17  Nat -> List ImageSemantics -> Type | Type
testdata/Builtins.lc 496:6-496:51  Type
testdata/Builtins.lc 496:24-496:27  Type
testdata/Builtins.lc 496:35-496:51  Type
testdata/Builtins.lc 496:36-496:50  Type
testdata/Builtins.lc 498:17-498:31  Type
testdata/Builtins.lc 498:35-498:39  Type
testdata/Builtins.lc 499:1-499:13  ImageSemantics->Type
testdata/Builtins.lc 499:15-499:20  ImageSemantics
testdata/Builtins.lc 499:15-501:29  ImageSemantics->Type | Type
testdata/Builtins.lc 499:26-499:27  Type | Type->Type
testdata/Builtins.lc 499:26-501:29  ImageSemantics->Type
testdata/Builtins.lc 500:26-500:27  Type | Type->V1
testdata/Builtins.lc 500:26-501:29  Type->Type -> ImageSemantics->Type
testdata/Builtins.lc 501:28-501:29  Type | Type->Type
testdata/Builtins.lc 503:19-503:33  Type
testdata/Builtins.lc 503:38-503:44  Type
testdata/Builtins.lc 503:39-503:43  Type
testdata/Builtins.lc 504:1-504:14  List ImageSemantics -> List Type
testdata/Builtins.lc 504:23-504:24  List ImageSemantics
testdata/Builtins.lc 504:23-505:37  List ImageSemantics -> List Type | List Type
testdata/Builtins.lc 504:30-504:33  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 504:30-504:46  List ImageSemantics -> List Type
testdata/Builtins.lc 504:30-504:48  List Type | Type->V1
testdata/Builtins.lc 504:30-505:37  (Type -> List Type) -> ImageSemantics -> List Type | List Type | List V1 -> List Type | V0 -> List V1 -> List Type
testdata/Builtins.lc 504:34-504:46  ImageSemantics->Type
testdata/Builtins.lc 504:47-504:48  List V3
testdata/Builtins.lc 505:19-505:22  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 505:19-505:35  List ImageSemantics -> List Type
testdata/Builtins.lc 505:19-505:37  List Type | Type -> List Type
testdata/Builtins.lc 505:23-505:35  ImageSemantics->Type
testdata/Builtins.lc 505:36-505:37  List ImageSemantics
testdata/Builtins.lc 507:39-507:53  Type
testdata/Builtins.lc 507:60-507:80  Type->ImageSemantics
testdata/Builtins.lc 507:82-507:99  Type
testdata/Builtins.lc 507:82-507:106  ImageSemantics->ImageSemantics | Type->ImageSemantics
testdata/Builtins.lc 507:105-507:106  ImageSemantics | ImageSemantics->ImageSemantics
testdata/Builtins.lc 509:1-509:11  {a : List ImageSemantics} -> {b:Nat} -> {c : List Type} -> {d : a ~ 'map Type ImageSemantics FragmentOperationSem c} -> HList c -> FragmentStream b (HList ('remSemantics' a)) -> FrameBuffer b a -> FrameBuffer b a
testdata/Builtins.lc 509:15-509:176  Type
testdata/Builtins.lc 509:28-509:31  Type
testdata/Builtins.lc 509:39-509:176  Type
testdata/Builtins.lc 509:40-509:44  Type
testdata/Builtins.lc 509:49-509:176  Type
testdata/Builtins.lc 509:50-509:51  V4
testdata/Builtins.lc 509:50-509:53  V3->Type
testdata/Builtins.lc 509:50-509:80  Type
testdata/Builtins.lc 509:52-509:53  {a} -> a -> a->Type
testdata/Builtins.lc 509:54-509:57  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 509:54-509:78  List Type -> List ImageSemantics
testdata/Builtins.lc 509:54-509:80  List ImageSemantics
testdata/Builtins.lc 509:58-509:78  Type->ImageSemantics
testdata/Builtins.lc 509:79-509:80  List Type
testdata/Builtins.lc 509:85-509:90  List Type -> Type
testdata/Builtins.lc 509:85-509:92  Type
testdata/Builtins.lc 509:85-509:176  Type
testdata/Builtins.lc 509:91-509:92  List Type
testdata/Builtins.lc 509:96-509:110  Nat -> Type->Type
testdata/Builtins.lc 509:96-509:112  Type->Type
testdata/Builtins.lc 509:96-509:138  Type
testdata/Builtins.lc 509:96-509:176  Type
testdata/Builtins.lc 509:111-509:112  Nat
testdata/Builtins.lc 509:114-509:119  List Type -> Type
testdata/Builtins.lc 509:114-509:137  Type
testdata/Builtins.lc 509:121-509:134  List ImageSemantics -> List Type
testdata/Builtins.lc 509:121-509:136  List Type
testdata/Builtins.lc 509:135-509:136  List ImageSemantics
testdata/Builtins.lc 509:142-509:153  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 509:142-509:155  List ImageSemantics -> Type
testdata/Builtins.lc 509:142-509:157  Type
testdata/Builtins.lc 509:142-509:176  Type
testdata/Builtins.lc 509:154-509:155  Nat
testdata/Builtins.lc 509:156-509:157  List ImageSemantics
testdata/Builtins.lc 509:161-509:172  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 509:161-509:174  List ImageSemantics -> Type
testdata/Builtins.lc 509:161-509:176  Type
testdata/Builtins.lc 509:173-509:174  Nat
testdata/Builtins.lc 509:175-509:176  List ImageSemantics
testdata/Builtins.lc 511:1-511:15  {a} -> {b} -> a -> b->(a, b)
testdata/Builtins.lc 511:24-511:32  (V3, V1)
testdata/Builtins.lc 511:25-511:28  V5
testdata/Builtins.lc 511:30-511:31  ((V1)) | V4
testdata/Builtins.lc 512:1-512:8  {a:Nat} -> {b : List Type} -> FrameBuffer a ('map Type ImageSemantics FragmentOperationSem b) -> (HList b, List (Fragment a (HList ('remSemantics' ('map Type ImageSemantics FragmentOperationSem b))))) -> FrameBuffer a ('map Type ImageSemantics FragmentOperationSem b)
testdata/Builtins.lc 512:13-512:21  V3
testdata/Builtins.lc 512:13-512:46  FrameBuffer V1 ('map Type ImageSemantics FragmentOperationSem V0)
testdata/Builtins.lc 512:25-512:35  {a : List ImageSemantics} -> {b:Nat} -> {c : List Type} -> {d : a ~ 'map Type ImageSemantics FragmentOperationSem c} -> HList c -> FragmentStream b (HList ('remSemantics' a)) -> FrameBuffer b a -> FrameBuffer b a
testdata/Builtins.lc 512:25-512:39  FragmentStream V1 (HList ('remSemantics' ('map Type ImageSemantics FragmentOperationSem V0))) -> FrameBuffer V2 ('map Type ImageSemantics FragmentOperationSem V1) -> FrameBuffer V3 ('map Type ImageSemantics FragmentOperationSem V2)
testdata/Builtins.lc 512:25-512:43  FrameBuffer V1 ('map Type ImageSemantics FragmentOperationSem V0) -> FrameBuffer V2 ('map Type ImageSemantics FragmentOperationSem V1)
testdata/Builtins.lc 512:25-512:46  FrameBuffer V1 ('map Type ImageSemantics FragmentOperationSem V0) | HList V2 -> V2 | V2 -> HList V2 -> V2
testdata/Builtins.lc 512:36-512:39  V12
testdata/Builtins.lc 512:40-512:43  V7
testdata/Builtins.lc 512:44-512:46  V13
testdata/Builtins.lc 516:28-516:42  Type
testdata/Builtins.lc 516:49-516:57  Type->ImageSemantics
testdata/Builtins.lc 516:59-516:64  Type
testdata/Builtins.lc 516:59-516:73  ImageSemantics->ImageSemantics | Type->ImageSemantics
testdata/Builtins.lc 516:72-516:73  ImageSemantics | ImageSemantics->ImageSemantics | Nat -> ImageSemantics->ImageSemantics
testdata/Builtins.lc 521:1-521:12  {a : List Type} -> {b : 'sameLayerCounts a} -> HList a -> FrameBuffer (ImageLC ('head Type a)) ('map Type ImageSemantics ImageSem a)
testdata/Builtins.lc 521:31-521:35  Type
testdata/Builtins.lc 521:40-521:121  Type
testdata/Builtins.lc 521:41-521:56  List Type -> Type
testdata/Builtins.lc 521:41-521:58  Type
testdata/Builtins.lc 521:57-521:58  List Type
testdata/Builtins.lc 521:63-521:68  List Type -> Type
testdata/Builtins.lc 521:63-521:70  Type
testdata/Builtins.lc 521:63-521:121  Type
testdata/Builtins.lc 521:69-521:70  List Type
testdata/Builtins.lc 521:74-521:85  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 521:74-521:104  List ImageSemantics -> Type
testdata/Builtins.lc 521:74-521:121  Type
testdata/Builtins.lc 521:87-521:94  Type->Nat
testdata/Builtins.lc 521:87-521:103  Nat
testdata/Builtins.lc 521:96-521:100  {a} -> List a -> a
testdata/Builtins.lc 521:96-521:102  Type
testdata/Builtins.lc 521:101-521:102  List Type
testdata/Builtins.lc 521:106-521:109  {a} -> {b} -> a->b -> List a -> List b
testdata/Builtins.lc 521:106-521:118  List Type -> List ImageSemantics
testdata/Builtins.lc 521:106-521:120  List ImageSemantics
testdata/Builtins.lc 521:110-521:118  Type->ImageSemantics
testdata/Builtins.lc 521:119-521:120  List Type
testdata/Builtins.lc 523:1-523:11  {a : List Type} -> {b : 'sameLayerCounts a} -> HList a -> FrameBuffer (ImageLC ('head Type a)) ('map Type ImageSemantics ImageSem a)
testdata/Builtins.lc 523:14-523:25  {a : List Type} -> {b : 'sameLayerCounts a} -> HList a -> FrameBuffer (ImageLC ('head Type a)) ('map Type ImageSemantics ImageSem a)
testdata/Builtins.lc 525:1-525:11  {a:Nat} -> {b : List Type} -> {c} -> HList b -> (c -> HList ('remSemantics' ('map Type ImageSemantics FragmentOperationSem b))) -> List (Vector a (Maybe (SimpleFragment c))) -> FrameBuffer a ('map Type ImageSemantics FragmentOperationSem b) -> FrameBuffer a ('map Type ImageSemantics FragmentOperationSem b)
testdata/Builtins.lc 525:34-525:44  {a : List ImageSemantics} -> {b:Nat} -> {c : List Type} -> {d : a ~ 'map Type ImageSemantics FragmentOperationSem c} -> HList c -> FragmentStream b (HList ('remSemantics' a)) -> FrameBuffer b a -> FrameBuffer b a
testdata/Builtins.lc 525:34-525:48  FragmentStream V1 (HList ('remSemantics' ('map Type ImageSemantics FragmentOperationSem V0))) -> FrameBuffer V2 ('map Type ImageSemantics FragmentOperationSem V1) -> FrameBuffer V3 ('map Type ImageSemantics FragmentOperationSem V2)
testdata/Builtins.lc 525:34-525:76  FrameBuffer V2 ('map Type ImageSemantics FragmentOperationSem V1) -> FrameBuffer V3 ('map Type ImageSemantics FragmentOperationSem V2)
testdata/Builtins.lc 525:34-525:79  FrameBuffer V2 ('map Type ImageSemantics FragmentOperationSem V1)
testdata/Builtins.lc 525:45-525:48  V9
testdata/Builtins.lc 525:50-525:62  {a} -> {b} -> {c:Nat} -> a->b -> List (Vector c (Maybe (SimpleFragment a))) -> List (Vector c (Maybe (SimpleFragment b)))
testdata/Builtins.lc 525:50-525:70  List (Vector V0 (Maybe (SimpleFragment V2))) -> List (Vector V1 (Maybe (SimpleFragment V2)))
testdata/Builtins.lc 525:50-525:75  List (Vector V2 (Maybe (SimpleFragment (HList ('remSemantics' ('map Type ImageSemantics FragmentOperationSem V1))))))
testdata/Builtins.lc 525:63-525:70  V10
testdata/Builtins.lc 525:71-525:75  V6
testdata/Builtins.lc 525:77-525:79  V4
testdata/Builtins.lc 528:1-528:9  {a:ImageSemantics} -> FrameBuffer 1 ('Cons a 'Nil) -> Image 1 a
testdata/Builtins.lc 528:24-528:35  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 528:24-528:37  List ImageSemantics -> Type
testdata/Builtins.lc 528:24-528:42  Type
testdata/Builtins.lc 528:24-528:55  Type
testdata/Builtins.lc 528:36-528:37  V1
testdata/Builtins.lc 528:38-528:42  List ImageSemantics
testdata/Builtins.lc 528:40-528:41  V2
testdata/Builtins.lc 528:46-528:51  Nat -> ImageSemantics->Type
testdata/Builtins.lc 528:46-528:53  ImageSemantics->Type
testdata/Builtins.lc 528:46-528:55  Type
testdata/Builtins.lc 528:52-528:53  V1
testdata/Builtins.lc 528:54-528:55  ImageSemantics
testdata/Builtins.lc 529:1-529:14  FrameBuffer 1 ('Cons ('Depth Float) ('Cons ('Color (Vec 4 Float)) 'Nil)) -> Image 1 ('Color (Vec 4 Float))
testdata/Builtins.lc 529:24-529:35  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 529:24-529:37  List ImageSemantics -> Type
testdata/Builtins.lc 529:24-529:76  Type
testdata/Builtins.lc 529:36-529:37  V1
testdata/Builtins.lc 529:38-529:76  List ImageSemantics
testdata/Builtins.lc 529:41-529:47  Type->ImageSemantics
testdata/Builtins.lc 529:41-529:53  ImageSemantics
testdata/Builtins.lc 529:48-529:53  Type
testdata/Builtins.lc 529:55-529:61  Type->ImageSemantics
testdata/Builtins.lc 529:55-529:75  ImageSemantics | List ImageSemantics
testdata/Builtins.lc 529:63-529:66  Nat -> Type->Type
testdata/Builtins.lc 529:63-529:68  Type->Type
testdata/Builtins.lc 529:63-529:74  Type
testdata/Builtins.lc 529:67-529:68  V1
testdata/Builtins.lc 529:69-529:74  Type
testdata/Builtins.lc 529:80-529:85  Nat -> ImageSemantics->Type
testdata/Builtins.lc 529:80-529:87  ImageSemantics->Type
testdata/Builtins.lc 529:80-529:109  Type
testdata/Builtins.lc 529:86-529:87  V1
testdata/Builtins.lc 529:89-529:94  Type->ImageSemantics
testdata/Builtins.lc 529:89-529:108  ImageSemantics
testdata/Builtins.lc 529:96-529:99  Nat -> Type->Type
testdata/Builtins.lc 529:96-529:101  Type->Type
testdata/Builtins.lc 529:96-529:107  Type
testdata/Builtins.lc 529:100-529:101  V1
testdata/Builtins.lc 529:102-529:107  Type
testdata/Builtins.lc 531:6-531:12  Type
testdata/Builtins.lc 531:6-532:12  Type
testdata/Builtins.lc 532:3-532:12  Output | Type | {a:Nat} -> {b : List ImageSemantics} -> FrameBuffer a b -> Output
testdata/Builtins.lc 532:26-532:37  Nat -> List ImageSemantics -> Type
testdata/Builtins.lc 532:26-532:39  List ImageSemantics -> Type
testdata/Builtins.lc 532:26-532:41  Type
testdata/Builtins.lc 532:26-532:51  Type
testdata/Builtins.lc 532:38-532:39  V3
testdata/Builtins.lc 532:40-532:41  V1
testdata/Builtins.lc 532:45-532:51  Type
testdata/Builtins.lc 534:1-534:12  {a:Nat} -> {b : List ImageSemantics} -> FrameBuffer a b -> Output
testdata/Builtins.lc 534:15-534:24  {a:Nat} -> {b : List ImageSemantics} -> FrameBuffer a b -> Output
testdata/Builtins.lc 540:6-540:13  Type
testdata/Builtins.lc 540:6-544:12  Type
testdata/Builtins.lc 541:3-541:16  String->Texture | Texture | Type
testdata/Builtins.lc 541:20-541:26  Type
testdata/Builtins.lc 542:20-542:27  Type
testdata/Builtins.lc 544:3-544:12  Texture | Type | Vec 2 Int -> Image 1 ('Color (Vec 4 Float)) -> Texture
testdata/Builtins.lc 544:20-544:23  Nat -> Type->Type
testdata/Builtins.lc 544:20-544:25  Type->Type
testdata/Builtins.lc 544:20-544:29  Type
testdata/Builtins.lc 544:24-544:25  V1
testdata/Builtins.lc 544:26-544:29  Type
testdata/Builtins.lc 545:20-545:25  Nat -> ImageSemantics->Type
testdata/Builtins.lc 545:20-545:27  ImageSemantics->Type
testdata/Builtins.lc 545:20-545:49  Type
testdata/Builtins.lc 545:20-546:27  Type
testdata/Builtins.lc 545:26-545:27  V1
testdata/Builtins.lc 545:29-545:34  Type->ImageSemantics
testdata/Builtins.lc 545:29-545:48  ImageSemantics
testdata/Builtins.lc 545:36-545:39  Nat -> Type->Type
testdata/Builtins.lc 545:36-545:41  Type->Type
testdata/Builtins.lc 545:36-545:47  Type
testdata/Builtins.lc 545:40-545:41  V1
testdata/Builtins.lc 545:42-545:47  Type
testdata/Builtins.lc 546:20-546:27  Type
testdata/Builtins.lc 548:6-548:12  Type
testdata/Builtins.lc 548:6-550:17  Type
testdata/Builtins.lc 549:5-549:16  Filter
testdata/Builtins.lc 550:5-550:17  Filter
testdata/Builtins.lc 552:6-552:14  Type
testdata/Builtins.lc 552:6-555:16  Type
testdata/Builtins.lc 553:5-553:11  EdgeMode
testdata/Builtins.lc 554:5-554:19  EdgeMode
testdata/Builtins.lc 555:5-555:16  EdgeMode
testdata/Builtins.lc 557:6-557:13  Type
testdata/Builtins.lc 557:6-557:23  Type
testdata/Builtins.lc 557:6-557:47  Type
testdata/Builtins.lc 557:16-557:23  Filter -> EdgeMode -> Texture->Sampler | Sampler | Type
testdata/Builtins.lc 557:24-557:30  Type
testdata/Builtins.lc 557:31-557:39  Type
testdata/Builtins.lc 557:40-557:47  Type
testdata/Builtins.lc 560:1-560:10  Sampler -> Vec 2 Float -> Vec 4 Float
testdata/Builtins.lc 560:14-560:21  Type
testdata/Builtins.lc 560:25-560:28  Nat -> Type->Type
testdata/Builtins.lc 560:25-560:30  Type->Type
testdata/Builtins.lc 560:25-560:36  Type
testdata/Builtins.lc 560:25-560:51  Type
testdata/Builtins.lc 560:29-560:30  V1
testdata/Builtins.lc 560:31-560:36  Type
testdata/Builtins.lc 560:40-560:43  Nat -> Type->Type
testdata/Builtins.lc 560:40-560:45  Type->Type
testdata/Builtins.lc 560:40-560:51  Type
testdata/Builtins.lc 560:44-560:45  V1
testdata/Builtins.lc 560:46-560:51  Type
testdata/Builtins.lc 564:1-564:20  {a} -> a->a
testdata/Builtins.lc 564:25-564:26  V1