Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Instance.Mat

Documentation

data Nat Source Comments #

Constructors

Z
S Nat

Instances

Instances details

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat type UN ('M :: Nat -> MatK a) ('M n :: MatK a) = n

type family (a :: Nat) + (b :: Nat) :: Nat where ... Source Comments #

Equations

'Z + b = b
('S a) + b = 'S (a + b)

type family (a :: Nat) * (b :: Nat) :: Nat where ... Source Comments #

Equations

'Z * b = 'Z
('S a) * b = b + (a * b)

data Vec (a :: Nat) b where Source Comments #

Constructors

Nil :: forall b. Vec 'Z b
Cons :: forall b (n :: Nat). b -> Vec n b -> Vec ('S n) b

Instances

Instances details

Applicative (Vec n) => Applicative (Vec ('S n)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods pure :: a -> Vec ('S n) a Comments # (<>) :: Vec ('S n) (a -> b) -> Vec ('S n) a -> Vec ('S n) b Comments # liftA2 :: (a -> b -> c) -> Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) c Comments # (>) :: Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) b Comments # (<*) :: Vec ('S n) a -> Vec ('S n) b -> Vec ('S n) a Comments #
Applicative (Vec 'Z) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods pure :: a -> Vec 'Z a Comments # (<>) :: Vec 'Z (a -> b) -> Vec 'Z a -> Vec 'Z b Comments # liftA2 :: (a -> b -> c) -> Vec 'Z a -> Vec 'Z b -> Vec 'Z c Comments # (>) :: Vec 'Z a -> Vec 'Z b -> Vec 'Z b Comments # (<*) :: Vec 'Z a -> Vec 'Z b -> Vec 'Z a Comments #
Functor (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fmap :: (a -> b) -> Vec n a -> Vec n b Comments # (<$) :: a -> Vec n b -> Vec n a Comments #
Foldable (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods fold :: Monoid m => Vec n m -> m Comments # foldMap :: Monoid m => (a -> m) -> Vec n a -> m Comments # foldMap' :: Monoid m => (a -> m) -> Vec n a -> m Comments # foldr :: (a -> b -> b) -> b -> Vec n a -> b Comments # foldr' :: (a -> b -> b) -> b -> Vec n a -> b Comments # foldl :: (b -> a -> b) -> b -> Vec n a -> b Comments # foldl' :: (b -> a -> b) -> b -> Vec n a -> b Comments # foldr1 :: (a -> a -> a) -> Vec n a -> a Comments # foldl1 :: (a -> a -> a) -> Vec n a -> a Comments # toList :: Vec n a -> [a] Comments # null :: Vec n a -> Bool Comments # length :: Vec n a -> Int Comments # elem :: Eq a => a -> Vec n a -> Bool Comments # maximum :: Ord a => Vec n a -> a Comments # minimum :: Ord a => Vec n a -> a Comments # sum :: Num a => Vec n a -> a Comments # product :: Num a => Vec n a -> a Comments #
Traversable (Vec n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) Comments # sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) Comments # mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) Comments # sequence :: Monad m => Vec n (m a) -> m (Vec n a) Comments #

data MatK a Source Comments #

Constructors

M Nat

Instances

Instances details

Num a => Monoidal (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Mat type Unit = 'M ('S 'Z) :: MatK a

Methods

withOb2 :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 ** b) => r) -> r Source Comments #

leftUnitor :: forall (a0 :: MatK a). Ob a0 => ((Unit :: MatK a) ** a0) ~> a0 Source Comments #

leftUnitorInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> ((Unit :: MatK a) ** a0) Source Comments #

rightUnitor :: forall (a0 :: MatK a). Ob a0 => (a0 ** (Unit :: MatK a)) ~> a0 Source Comments #

rightUnitorInv :: forall (a0 :: MatK a). Ob a0 => a0 ~> (a0 ** (Unit :: MatK a)) Source Comments #

associator :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => ((a0 ** b) ** c) ~> (a0 ** (b ** c)) Source Comments #

associatorInv :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => (a0 ** (b ** c)) ~> ((a0 ** b) ** c) Source Comments #

Num a => SymMonoidal (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

swap :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 ** b) ~> (b ** a0) Source Comments #

Num a => CategoryOf (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Mat type (~>) = Mat :: MatK a -> MatK a -> Type

Num a => HasBinaryCoproducts (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObCoprod :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 || b) => r) -> r Source Comments #

lft :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => a0 ~> (a0 || b) Source Comments #

rgt :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => b ~> (a0 || b) Source Comments #

(|||) :: forall (x :: MatK a) (a0 :: MatK a) (y :: MatK a). (x ~> a0) -> (y ~> a0) -> (x || y) ~> a0 Source Comments #

(+++) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (b ~> y) -> (a0 || b) ~> (x || y) Source Comments #

Num a => HasBinaryProducts (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

withObProd :: forall (a0 :: MatK a) (b :: MatK a) r. (Ob a0, Ob b) => (Ob (a0 && b) => r) -> r Source Comments #

fst :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> a0 Source Comments #

snd :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (a0 && b) ~> b Source Comments #

(&&&) :: forall (a0 :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (a0 ~> y) -> a0 ~> (x && y) Source Comments #

(***) :: forall (a0 :: MatK a) (b :: MatK a) (x :: MatK a) (y :: MatK a). (a0 ~> x) -> (b ~> y) -> (a0 && b) ~> (x && y) Source Comments #

Num a => CompactClosed (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

distribDual :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => Dual (a0 ** b) ~> (Dual a0 ** Dual b) Source Comments #

dualUnit :: Dual (Unit :: MatK a) ~> (Unit :: MatK a) Source Comments #

Num a => StarAutonomous (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dual :: forall (a0 :: MatK a) (b :: MatK a). (a0 ~> b) -> Dual b ~> Dual a0 Source Comments #

dualInv :: forall (a0 :: MatK a) (b :: MatK a). (Ob a0, Ob b) => (Dual a0 ~> Dual b) -> b ~> a0 Source Comments #

linDist :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => ((a0 ** b) ~> Dual c) -> a0 ~> Dual (b ** c) Source Comments #

linDistInv :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). (Ob a0, Ob b, Ob c) => (a0 ~> Dual (b ** c)) -> (a0 ** b) ~> Dual c Source Comments #

Num a => Closed (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

curry' :: forall (a0 :: MatK a) (b :: MatK a) (c :: MatK a). Obj a0 -> Obj b -> ((a0 ** b) ~> c) -> a0 ~> (b ~~> c) Source Comments #

uncurry' :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Obj b -> Obj c -> (a0 ~> (b ~~> c)) -> (a0 ** b) ~> c Source Comments #

(^^^) :: forall (b :: MatK a) (y :: MatK a) (x :: MatK a) (a0 :: MatK a). (b ~> y) -> (x ~> a0) -> (a0 ~~> b) ~> (x ~~> y) Source Comments #

Num a => HasInitialObject (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Mat type InitialObject = 'M 'Z :: MatK a

Methods

initiate :: forall (a0 :: MatK a). Ob a0 => (InitialObject :: MatK a) ~> a0 Source Comments #

initiate' :: forall (a' :: MatK a) (a0 :: MatK a). (a' ~> a0) -> (InitialObject :: MatK a) ~> a0 Source Comments #

Num a => HasTerminalObject (MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Mat type TerminalObject = 'M 'Z :: MatK a

Methods

terminate :: forall (a0 :: MatK a). Ob a0 => a0 ~> (TerminalObject :: MatK a) Source Comments #

terminate' :: forall (a0 :: MatK a) (a' :: MatK a). (a0 ~> a') -> a0 ~> (TerminalObject :: MatK a) Source Comments #

RealFloat a => DaggerProfunctor (Mat :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dagger :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Mat a0 b -> Mat b a0 Source Comments #

Num a => DaggerProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dagger :: forall (a0 :: MatK a) (b :: MatK a). Mat a0 b -> Mat b a0 Source Comments #

Num a => TracedMonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

trace :: forall (u :: MatK a) (x :: MatK a) (y :: MatK a). (Ob x, Ob y, Ob u) => Mat (x ** u) (y ** u) -> Mat x y Source Comments #

trace' :: forall (x :: MatK a) (x' :: MatK a) (y :: MatK a) (y' :: MatK a) (u :: MatK a) (u' :: MatK a). (x ~> x') -> (y ~> y') -> (u ~> u') -> Mat (x' ** u') (y ** u) -> Mat x y' Source Comments #

Num a => Promonad (Mat :: MatK a -> MatK a -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

id :: forall (a0 :: MatK a). Ob a0 => Mat a0 a0 Source Comments #

(.) :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Mat b c -> Mat a0 b -> Mat a0 c Source Comments #

Num a => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

par0 :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Comments #

par :: forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a). Mat x1 x2 -> Mat y1 y2 -> Mat (x1 ** y1) (x2 ** y2) Source Comments #

Num a => Profunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

Methods

dimap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a) (d :: MatK a). (c ~> a0) -> (b ~> d) -> Mat a0 b -> Mat c d Source Comments #

(\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Comments #

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) = n

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Unit = 'M ('S 'Z) :: MatK a

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (~>) = Mat :: MatK a -> MatK a -> Type

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type InitialObject = 'M 'Z :: MatK a

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type TerminalObject = 'M 'Z :: MatK a

type Ob (n :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Ob (n :: MatK a) = (Is ('M :: Nat -> MatK a) n, IsNat (UN ('M :: Nat -> MatK a) n))

type Dual (n :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type Dual (n :: MatK a) = n

type (x :: MatK a) ~~> (y :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type (x :: MatK a) ~~> (y :: MatK a) = ExpSA x y

type ('M x :: MatK a) ** ('M y :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) ** ('M y :: MatK a) = 'M (y * x) :: MatK a

type ('M x :: MatK a) || ('M y :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) || ('M y :: MatK a) = 'M (x + y) :: MatK a

type ('M x :: MatK a) && ('M y :: MatK a) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Mat

type ('M x :: MatK a) && ('M y :: MatK a) = 'M (x + y) :: MatK a

data Mat (b :: MatK a) (c :: MatK a) where Source Comments #

Constructors

Mat :: forall {a} {b :: MatK a} {c :: MatK a} (m :: Nat) (n :: Nat). (Ob b, Ob c, b ~ ('M m :: MatK a), c ~ ('M n :: MatK a)) => Vec n (Vec m a) -> Mat b c

Instances

Instances details

RealFloat a => DaggerProfunctor (Mat :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dagger :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Mat a0 b -> Mat b a0 Source Comments #
Num a => DaggerProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dagger :: forall (a0 :: MatK a) (b :: MatK a). Mat a0 b -> Mat b a0 Source Comments #
Num a => TracedMonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods trace :: forall (u :: MatK a) (x :: MatK a) (y :: MatK a). (Ob x, Ob y, Ob u) => Mat (x u) (y u) -> Mat x y Source Comments # trace' :: forall (x :: MatK a) (x' :: MatK a) (y :: MatK a) (y' :: MatK a) (u :: MatK a) (u' :: MatK a). (x ~> x') -> (y ~> y') -> (u ~> u') -> Mat (x' u') (y u) -> Mat x y' Source Comments #
Num a => Promonad (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods id :: forall (a0 :: MatK a). Ob a0 => Mat a0 a0 Source Comments # (.) :: forall (b :: MatK a) (c :: MatK a) (a0 :: MatK a). Mat b c -> Mat a0 b -> Mat a0 c Source Comments #
Num a => MonoidalProfunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods par0 :: Mat (Unit :: MatK a) (Unit :: MatK a) Source Comments # par :: forall (x1 :: MatK a) (x2 :: MatK a) (y1 :: MatK a) (y2 :: MatK a). Mat x1 x2 -> Mat y1 y2 -> Mat (x1 y1) (x2 y2) Source Comments #
Num a => Profunctor (Mat :: MatK a -> MatK a -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods dimap :: forall (c :: MatK a) (a0 :: MatK a) (b :: MatK a) (d :: MatK a). (c ~> a0) -> (b ~> d) -> Mat a0 b -> Mat c d Source Comments # (\\) :: forall (a0 :: MatK a) (b :: MatK a) r. ((Ob a0, Ob b) => r) -> Mat a0 b -> r Source Comments #

apply :: forall a (m :: Nat) (n :: Nat). (Num a, Applicative (Vec m)) => Vec n (Vec m a) -> Vec m a -> Vec n a Source Comments #

class (Applicative (Vec n), (n + 'Z) ~ n, (n * 'Z) ~ 'Z, (n * 'S 'Z) ~ n) => IsNat (n :: Nat) where Source Comments #

Methods

matId :: Num a => Vec n (Vec n a) Source Comments #

zero :: Num a => Vec n a Source Comments #

append :: forall a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a Source Comments #

split :: forall (m :: Nat) a. Vec (n + m) a -> (Vec n a, Vec m a) Source Comments #

concatMap :: forall (m :: Nat) a b. IsNat m => (a -> Vec m b) -> Vec n a -> Vec (n * m) b Source Comments #

unConcatMap :: forall (m :: Nat) b a. IsNat m => (Vec m b -> a) -> Vec (n * m) b -> Vec n a Source Comments #

withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat (n + m) => r) -> r Source Comments #

withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat (n * m) => r) -> r Source Comments #

withPlusSucc :: forall (m :: Nat) r. IsNat m => ((n + 'S m) ~ 'S (n + m) => r) -> r Source Comments #

withMultSucc :: forall (m :: Nat) r. IsNat m => ((n * 'S m) ~ (n + (n * m)) => r) -> r Source Comments #

withPlusSym :: forall (m :: Nat) r. IsNat m => ((n + m) ~ (m + n) => r) -> r Source Comments #

withMultSym :: forall (m :: Nat) r. IsNat m => ((n * m) ~ (m * n) => r) -> r Source Comments #

withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) + o) ~ (n + (m + o)) => r) -> r Source Comments #

withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n * m) * o) ~ (n * (m * o)) => r) -> r Source Comments #

withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => (((n + m) * o) ~ ((n * o) + (m * o)) => r) -> r Source Comments #

Instances

Instances details

IsNat 'Z Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods matId :: Num a => Vec 'Z (Vec 'Z a) Source Comments # zero :: Num a => Vec 'Z a Source Comments # append :: forall a (m :: Nat). Vec 'Z a -> Vec m a -> Vec ('Z + m) a Source Comments # split :: forall (m :: Nat) a. Vec ('Z + m) a -> (Vec 'Z a, Vec m a) Source Comments # concatMap :: forall (m :: Nat) a b. IsNat m => (a -> Vec m b) -> Vec 'Z a -> Vec ('Z * m) b Source Comments # unConcatMap :: forall (m :: Nat) b a. IsNat m => (Vec m b -> a) -> Vec ('Z * m) b -> Vec 'Z a Source Comments # withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z + m) => r) -> r Source Comments # withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('Z * m) => r) -> r Source Comments # withPlusSucc :: forall (m :: Nat) r. IsNat m => (('Z + 'S m) ~ 'S ('Z + m) => r) -> r Source Comments # withMultSucc :: forall (m :: Nat) r. IsNat m => (('Z * 'S m) ~ ('Z + ('Z * m)) => r) -> r Source Comments # withPlusSym :: forall (m :: Nat) r. IsNat m => (('Z + m) ~ (m + 'Z) => r) -> r Source Comments # withMultSym :: forall (m :: Nat) r. IsNat m => (('Z * m) ~ (m * 'Z) => r) -> r Source Comments # withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z + m) + o) ~ ('Z + (m + o)) => r) -> r Source Comments # withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z * m) * o) ~ ('Z * (m * o)) => r) -> r Source Comments # withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('Z + m) * o) ~ (('Z * o) + (m * o)) => r) -> r Source Comments #
IsNat n => IsNat ('S n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Mat Methods matId :: Num a => Vec ('S n) (Vec ('S n) a) Source Comments # zero :: Num a => Vec ('S n) a Source Comments # append :: forall a (m :: Nat). Vec ('S n) a -> Vec m a -> Vec ('S n + m) a Source Comments # split :: forall (m :: Nat) a. Vec ('S n + m) a -> (Vec ('S n) a, Vec m a) Source Comments # concatMap :: forall (m :: Nat) a b. IsNat m => (a -> Vec m b) -> Vec ('S n) a -> Vec ('S n * m) b Source Comments # unConcatMap :: forall (m :: Nat) b a. IsNat m => (Vec m b -> a) -> Vec ('S n * m) b -> Vec ('S n) a Source Comments # withPlusNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n + m) => r) -> r Source Comments # withMultNat :: forall (m :: Nat) r. IsNat m => (IsNat ('S n * m) => r) -> r Source Comments # withPlusSucc :: forall (m :: Nat) r. IsNat m => (('S n + 'S m) ~ 'S ('S n + m) => r) -> r Source Comments # withMultSucc :: forall (m :: Nat) r. IsNat m => (('S n * 'S m) ~ ('S n + ('S n * m)) => r) -> r Source Comments # withPlusSym :: forall (m :: Nat) r. IsNat m => (('S n + m) ~ (m + 'S n) => r) -> r Source Comments # withMultSym :: forall (m :: Nat) r. IsNat m => (('S n * m) ~ (m * 'S n) => r) -> r Source Comments # withAssocPlus :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n + m) + o) ~ ('S n + (m + o)) => r) -> r Source Comments # withAssocMult :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n * m) * o) ~ ('S n * (m * o)) => r) -> r Source Comments # withDist :: forall (m :: Nat) (o :: Nat) r. (IsNat m, IsNat o) => ((('S n + m) * o) ~ (('S n * o) + (m * o)) => r) -> r Source Comments #

withNat :: forall (n :: Nat) a r. Vec n a -> (IsNat n => r) -> r Source Comments #

mat :: forall {a1} (m :: Nat) (n :: Nat) a2. Ob ('M m :: MatK a1) => Vec n (Vec m a2) -> Mat ('M m :: MatK a2) ('M n :: MatK a2) Source Comments #