Mezzo.Model.Prim

Vectors and matrices

data Vector

data Times n

data Elem

type family (v :: t) ** (d :: Nat) :: Elem t d where ...

data OptVector

type family Head (v :: OptVector t n) :: t where ...

type family Head' (v :: Vector t n) :: t where ...

type family Last (v :: OptVector t n) :: t where ...

type family Tail' (v :: Vector t n) :: Vector t (n - 1) where ...

type family Init' (v :: Vector t n) :: Vector t (n - 1) where ...

type family Length (v :: OptVector t n) :: Nat where ...

type family Length' (v :: Vector t n) :: Nat where ...

type Matrix t p q

type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where ...

type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where ...

type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where ...

type family (a :: t) +*+ (n :: Nat) :: OptVector t n where ...

type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where ...

type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where ...

type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where ...

type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where ...

Logic and arithmetic

type family If (b :: Bool) (t :: k) (e :: k) :: k where ...

type family Not (a :: Bool) :: Bool where ...

type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where ...

type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where ...

type family (a :: k) .~. (b :: k) :: Bool where ...

type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where ...

type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where ...

Constraints

type Valid

type Invalid

type family AllSatisfy (c :: a -> Constraint) (xs :: OptVector a n) :: Constraint where ...

type family AllPairsSatisfy (c :: a -> b -> Constraint) (xs :: OptVector a n) (ys :: OptVector b n) :: Constraint where ...

type family AllPairsSatisfy' (c :: a -> b -> Constraint) (xs :: Vector a n) (ys :: Vector b n) :: Constraint where ...

type family SatisfiesAll (cs :: [a -> Constraint]) (xs :: a) :: Constraint where ...

type family AllSatisfyAll (c1 :: [a -> Constraint]) (xs :: Vector a n) :: Constraint where ...