Copyright	(c) Dennis Gosnell 2018
License	BSD3
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Termonad.Config.Vec

Description

This is a small library of dependent types. It provides indexed types like Fin, Vec, and Matrix.

This is mainly used in Termonad for Termonad.Config.Colour to represent length-indexed colour lists.

This module implements a subset of the functionality from the abandoned type-combinators library. Ideally this module would be split out to a separate package. If you're interested in working on something like this, please see this issue on Github.

Synopsis

data Peano
- = Z
- | S Peano
type ZSym0 = Z
type SSym1 (t6989586621679475479 :: Peano) = S t6989586621679475479
data SSym0 :: (~>) Peano Peano where
- SSym0KindInference :: forall t6989586621679475479 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679475479
type family N0 :: Peano where ...
type N0Sym0 = N0
type family N1 :: Peano where ...
type N1Sym0 = N1
type family N2 :: Peano where ...
type N2Sym0 = N2
type family N3 :: Peano where ...
type N3Sym0 = N3
type family N4 :: Peano where ...
type N4Sym0 = N4
type family N5 :: Peano where ...
type N5Sym0 = N5
type family N6 :: Peano where ...
type N6Sym0 = N6
type family N7 :: Peano where ...
type N7Sym0 = N7
type family N8 :: Peano where ...
type N8Sym0 = N8
type family N9 :: Peano where ...
type N9Sym0 = N9
type family N10 :: Peano where ...
type N10Sym0 = N10
type family SubtractPeano (a :: Peano) (a :: Peano) :: Peano where ...
data SubtractPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where
- SubtractPeanoSym0KindInference :: forall a6989586621679475487 arg. SameKind (Apply SubtractPeanoSym0 arg) (SubtractPeanoSym1 arg) => SubtractPeanoSym0 a6989586621679475487
data SubtractPeanoSym1 (a6989586621679475487 :: Peano) :: (~>) Peano Peano where
- SubtractPeanoSym1KindInference :: forall a6989586621679475487 a6989586621679475488 arg. SameKind (Apply (SubtractPeanoSym1 a6989586621679475487) arg) (SubtractPeanoSym2 a6989586621679475487 arg) => SubtractPeanoSym1 a6989586621679475487 a6989586621679475488
type SubtractPeanoSym2 (a6989586621679475487 :: Peano) (a6989586621679475488 :: Peano) = SubtractPeano a6989586621679475487 a6989586621679475488
type family AddPeano (a :: Peano) (a :: Peano) :: Peano where ...
data AddPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where
- AddPeanoSym0KindInference :: forall a6989586621679475494 arg. SameKind (Apply AddPeanoSym0 arg) (AddPeanoSym1 arg) => AddPeanoSym0 a6989586621679475494
data AddPeanoSym1 (a6989586621679475494 :: Peano) :: (~>) Peano Peano where
- AddPeanoSym1KindInference :: forall a6989586621679475494 a6989586621679475495 arg. SameKind (Apply (AddPeanoSym1 a6989586621679475494) arg) (AddPeanoSym2 a6989586621679475494 arg) => AddPeanoSym1 a6989586621679475494 a6989586621679475495
type AddPeanoSym2 (a6989586621679475494 :: Peano) (a6989586621679475495 :: Peano) = AddPeano a6989586621679475494 a6989586621679475495
type family MultPeano (a :: Peano) (a :: Peano) :: Peano where ...
data MultPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where
- MultPeanoSym0KindInference :: forall a6989586621679475481 arg. SameKind (Apply MultPeanoSym0 arg) (MultPeanoSym1 arg) => MultPeanoSym0 a6989586621679475481
data MultPeanoSym1 (a6989586621679475481 :: Peano) :: (~>) Peano Peano where
- MultPeanoSym1KindInference :: forall a6989586621679475481 a6989586621679475482 arg. SameKind (Apply (MultPeanoSym1 a6989586621679475481) arg) (MultPeanoSym2 a6989586621679475481 arg) => MultPeanoSym1 a6989586621679475481 a6989586621679475482
type MultPeanoSym2 (a6989586621679475481 :: Peano) (a6989586621679475482 :: Peano) = MultPeano a6989586621679475481 a6989586621679475482
type family N24 :: Peano where ...
type N24Sym0 = N24
type family Compare_6989586621679477240 (a :: Peano) (a :: Peano) :: Ordering where ...
type Compare_6989586621679477240Sym2 (a6989586621679477238 :: Peano) (a6989586621679477239 :: Peano) = Compare_6989586621679477240 a6989586621679477238 a6989586621679477239
data Compare_6989586621679477240Sym1 (a6989586621679477238 :: Peano) :: (~>) Peano Ordering where
- Compare_6989586621679477240Sym1KindInference :: forall a6989586621679477238 a6989586621679477239 arg. SameKind (Apply (Compare_6989586621679477240Sym1 a6989586621679477238) arg) (Compare_6989586621679477240Sym2 a6989586621679477238 arg) => Compare_6989586621679477240Sym1 a6989586621679477238 a6989586621679477239
data Compare_6989586621679477240Sym0 :: (~>) Peano ((~>) Peano Ordering) where
- Compare_6989586621679477240Sym0KindInference :: forall a6989586621679477238 arg. SameKind (Apply Compare_6989586621679477240Sym0 arg) (Compare_6989586621679477240Sym1 arg) => Compare_6989586621679477240Sym0 a6989586621679477238
type family ShowsPrec_6989586621679477933 (a :: Nat) (a :: Peano) (a :: Symbol) :: Symbol where ...
type ShowsPrec_6989586621679477933Sym3 (a6989586621679477930 :: Nat) (a6989586621679477931 :: Peano) (a6989586621679477932 :: Symbol) = ShowsPrec_6989586621679477933 a6989586621679477930 a6989586621679477931 a6989586621679477932
data ShowsPrec_6989586621679477933Sym2 (a6989586621679477930 :: Nat) (a6989586621679477931 :: Peano) :: (~>) Symbol Symbol where
- ShowsPrec_6989586621679477933Sym2KindInference :: forall a6989586621679477930 a6989586621679477931 a6989586621679477932 arg. SameKind (Apply (ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931) arg) (ShowsPrec_6989586621679477933Sym3 a6989586621679477930 a6989586621679477931 arg) => ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931 a6989586621679477932
data ShowsPrec_6989586621679477933Sym1 (a6989586621679477930 :: Nat) :: (~>) Peano ((~>) Symbol Symbol) where
- ShowsPrec_6989586621679477933Sym1KindInference :: forall a6989586621679477930 a6989586621679477931 arg. SameKind (Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930) arg) (ShowsPrec_6989586621679477933Sym2 a6989586621679477930 arg) => ShowsPrec_6989586621679477933Sym1 a6989586621679477930 a6989586621679477931
data ShowsPrec_6989586621679477933Sym0 :: (~>) Nat ((~>) Peano ((~>) Symbol Symbol)) where
- ShowsPrec_6989586621679477933Sym0KindInference :: forall a6989586621679477930 arg. SameKind (Apply ShowsPrec_6989586621679477933Sym0 arg) (ShowsPrec_6989586621679477933Sym1 arg) => ShowsPrec_6989586621679477933Sym0 a6989586621679477930
type family TFHelper_6989586621679478474 (a :: Peano) (a :: Peano) :: Peano where ...
type TFHelper_6989586621679478474Sym2 (a6989586621679478472 :: Peano) (a6989586621679478473 :: Peano) = TFHelper_6989586621679478474 a6989586621679478472 a6989586621679478473
data TFHelper_6989586621679478474Sym1 (a6989586621679478472 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679478474Sym1KindInference :: forall a6989586621679478472 a6989586621679478473 arg. SameKind (Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472) arg) (TFHelper_6989586621679478474Sym2 a6989586621679478472 arg) => TFHelper_6989586621679478474Sym1 a6989586621679478472 a6989586621679478473
data TFHelper_6989586621679478474Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679478474Sym0KindInference :: forall a6989586621679478472 arg. SameKind (Apply TFHelper_6989586621679478474Sym0 arg) (TFHelper_6989586621679478474Sym1 arg) => TFHelper_6989586621679478474Sym0 a6989586621679478472
type family TFHelper_6989586621679478490 (a :: Peano) (a :: Peano) :: Peano where ...
type TFHelper_6989586621679478490Sym2 (a6989586621679478488 :: Peano) (a6989586621679478489 :: Peano) = TFHelper_6989586621679478490 a6989586621679478488 a6989586621679478489
data TFHelper_6989586621679478490Sym1 (a6989586621679478488 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679478490Sym1KindInference :: forall a6989586621679478488 a6989586621679478489 arg. SameKind (Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488) arg) (TFHelper_6989586621679478490Sym2 a6989586621679478488 arg) => TFHelper_6989586621679478490Sym1 a6989586621679478488 a6989586621679478489
data TFHelper_6989586621679478490Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679478490Sym0KindInference :: forall a6989586621679478488 arg. SameKind (Apply TFHelper_6989586621679478490Sym0 arg) (TFHelper_6989586621679478490Sym1 arg) => TFHelper_6989586621679478490Sym0 a6989586621679478488
type family TFHelper_6989586621679478506 (a :: Peano) (a :: Peano) :: Peano where ...
type TFHelper_6989586621679478506Sym2 (a6989586621679478504 :: Peano) (a6989586621679478505 :: Peano) = TFHelper_6989586621679478506 a6989586621679478504 a6989586621679478505
data TFHelper_6989586621679478506Sym1 (a6989586621679478504 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679478506Sym1KindInference :: forall a6989586621679478504 a6989586621679478505 arg. SameKind (Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504) arg) (TFHelper_6989586621679478506Sym2 a6989586621679478504 arg) => TFHelper_6989586621679478506Sym1 a6989586621679478504 a6989586621679478505
data TFHelper_6989586621679478506Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679478506Sym0KindInference :: forall a6989586621679478504 arg. SameKind (Apply TFHelper_6989586621679478506Sym0 arg) (TFHelper_6989586621679478506Sym1 arg) => TFHelper_6989586621679478506Sym0 a6989586621679478504
type family Abs_6989586621679478521 (a :: Peano) :: Peano where ...
type Abs_6989586621679478521Sym1 (a6989586621679478520 :: Peano) = Abs_6989586621679478521 a6989586621679478520
data Abs_6989586621679478521Sym0 :: (~>) Peano Peano where
- Abs_6989586621679478521Sym0KindInference :: forall a6989586621679478520 arg. SameKind (Apply Abs_6989586621679478521Sym0 arg) (Abs_6989586621679478521Sym1 arg) => Abs_6989586621679478521Sym0 a6989586621679478520
type family Signum_6989586621679478530 (a :: Peano) :: Peano where ...
type Signum_6989586621679478530Sym1 (a6989586621679478529 :: Peano) = Signum_6989586621679478530 a6989586621679478529
data Signum_6989586621679478530Sym0 :: (~>) Peano Peano where
- Signum_6989586621679478530Sym0KindInference :: forall a6989586621679478529 arg. SameKind (Apply Signum_6989586621679478530Sym0 arg) (Signum_6989586621679478530Sym1 arg) => Signum_6989586621679478530Sym0 a6989586621679478529
type family Let6989586621679478541Scrutinee_6989586621679463510 n where ...
type Let6989586621679478541Scrutinee_6989586621679463510Sym1 n6989586621679478540 = Let6989586621679478541Scrutinee_6989586621679463510 n6989586621679478540
data Let6989586621679478541Scrutinee_6989586621679463510Sym0 n6989586621679478540 where
- Let6989586621679478541Scrutinee_6989586621679463510Sym0KindInference :: forall n6989586621679478540 arg. SameKind (Apply Let6989586621679478541Scrutinee_6989586621679463510Sym0 arg) (Let6989586621679478541Scrutinee_6989586621679463510Sym1 arg) => Let6989586621679478541Scrutinee_6989586621679463510Sym0 n6989586621679478540
type family Let6989586621679478545Scrutinee_6989586621679463512 n where ...
type Let6989586621679478545Scrutinee_6989586621679463512Sym1 n6989586621679478540 = Let6989586621679478545Scrutinee_6989586621679463512 n6989586621679478540
data Let6989586621679478545Scrutinee_6989586621679463512Sym0 n6989586621679478540 where
- Let6989586621679478545Scrutinee_6989586621679463512Sym0KindInference :: forall n6989586621679478540 arg. SameKind (Apply Let6989586621679478545Scrutinee_6989586621679463512Sym0 arg) (Let6989586621679478545Scrutinee_6989586621679463512Sym1 arg) => Let6989586621679478545Scrutinee_6989586621679463512Sym0 n6989586621679478540
type family Case_6989586621679478547 n t where ...
type family Case_6989586621679478543 n t where ...
type family FromInteger_6989586621679478536 (a :: Nat) :: Peano where ...
type FromInteger_6989586621679478536Sym1 (a6989586621679478535 :: Nat) = FromInteger_6989586621679478536 a6989586621679478535
data FromInteger_6989586621679478536Sym0 :: (~>) Nat Peano where
- FromInteger_6989586621679478536Sym0KindInference :: forall a6989586621679478535 arg. SameKind (Apply FromInteger_6989586621679478536Sym0 arg) (FromInteger_6989586621679478536Sym1 arg) => FromInteger_6989586621679478536Sym0 a6989586621679478535
type family Equals_6989586621679478552 (a :: Peano) (b :: Peano) :: Bool where ...
data SPeano :: Peano -> Type where
- SZ :: SPeano Z
- SS :: forall (n :: Peano). (Sing (n :: Peano)) -> SPeano (S n)
sAddPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply AddPeanoSym0 t) t :: Peano)
sSubtractPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply SubtractPeanoSym0 t) t :: Peano)
sMultPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply MultPeanoSym0 t) t :: Peano)
sN0 :: Sing (N0Sym0 :: Peano)
sN1 :: Sing (N1Sym0 :: Peano)
sN2 :: Sing (N2Sym0 :: Peano)
sN3 :: Sing (N3Sym0 :: Peano)
sN4 :: Sing (N4Sym0 :: Peano)
sN5 :: Sing (N5Sym0 :: Peano)
sN6 :: Sing (N6Sym0 :: Peano)
sN7 :: Sing (N7Sym0 :: Peano)
sN8 :: Sing (N8Sym0 :: Peano)
sN9 :: Sing (N9Sym0 :: Peano)
sN10 :: Sing (N10Sym0 :: Peano)
sN24 :: Sing (N24Sym0 :: Peano)
n24 :: Peano
n10 :: Peano
n9 :: Peano
n8 :: Peano
n7 :: Peano
n6 :: Peano
n5 :: Peano
n4 :: Peano
n3 :: Peano
n2 :: Peano
n1 :: Peano
n0 :: Peano
multPeano :: Peano -> Peano -> Peano
subtractPeano :: Peano -> Peano -> Peano
addPeano :: Peano -> Peano -> Peano
ltSuccProof :: forall (n :: Peano) (m :: Peano) proxy. ('S n < 'S m) ~ 'True => proxy n -> proxy m -> (n < m) :~: 'True
data Fin :: Peano -> Type where
- FZ :: forall (n :: Peano). Fin ('S n)
- FS :: forall (n :: Peano). !(Fin n) -> Fin ('S n)
toIntFin :: Fin n -> Int
fin :: forall total n. (n < total) ~ 'True => Sing total -> Sing n -> Fin total
fin_ :: forall total n. (SingI total, (n < total) ~ 'True) => Sing n -> Fin total
data SFin :: forall n. Fin n -> Type where
- SFZ :: SFin 'FZ
- SFS :: SFin n -> SFin ('FS n)
data IFin :: Peano -> Peano -> Type where
- IFZ :: forall (n :: Peano). IFin ('S n) 'Z
- IFS :: forall (n :: Peano) (m :: Peano). !(IFin n m) -> IFin ('S n) ('S m)
toFinIFin :: IFin n m -> Fin n
toIntIFin :: IFin n m -> Int
ifin :: forall total n. (n < total) ~ 'True => Sing total -> Sing n -> IFin total n
ifin_ :: forall total n. (SingI total, (n < total) ~ 'True) => Sing n -> IFin total n
data SIFin :: forall n m. IFin n m -> Type where
- SIFZ :: SIFin 'IFZ
- SIFS :: SIFin x -> SIFin ('IFS x)
data HList :: (k -> Type) -> [k] -> Type where
- EmptyHList :: HList f '[]
- (:<) :: forall (f :: k -> Type) (a :: k) (as :: [k]). f a -> HList f as -> HList f (a ': as)
pattern ConsHList :: (f a :: Type) -> HList f as -> HList f (a ': as)
data Vec (n :: Peano) :: Type -> Type where
- EmptyVec :: Vec 'Z a
- (:*) :: !a -> !(Vec n a) -> Vec ('S n) a
pattern ConsVec :: (a :: Type) -> Vec n a -> Vec ('S n) a
genVec_ :: SingI n => (Fin n -> a) -> Vec n a
genVec :: SPeano n -> (Fin n -> a) -> Vec n a
indexVec :: Fin n -> Vec n a -> a
singletonVec :: a -> Vec N1 a
replaceVec :: Sing n -> a -> Vec n a
imapVec :: forall n a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
replaceVec_ :: SingI n => a -> Vec n a
apVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
onHeadVec :: (a -> a) -> Vec ('S n) a -> Vec ('S n) a
dropVec :: Sing m -> Vec (m + n) a -> Vec n a
takeVec :: IFin n m -> Vec n a -> Vec m a
updateAtVec :: Fin n -> (a -> a) -> Vec n a -> Vec n a
setAtVec :: Fin n -> a -> Vec n a -> Vec n a
fromListVec :: Sing n -> [a] -> Maybe (Vec n a)
fromListVec_ :: SingI n => [a] -> Maybe (Vec n a)
unsafeFromListVec :: Sing n -> [a] -> Vec n a
unsafeFromListVec_ :: SingI n => [a] -> Vec n a
type family MatrixTF (ns :: [Peano]) (a :: Type) :: Type where ...
newtype Matrix ns a = Matrix {
- unMatrix :: MatrixTF ns a
}
type MatrixTFSym2 (ns :: [Peano]) (t :: Type) = MatrixTF ns t :: Type
data MatrixTFSym1 (ns :: [Peano]) (z :: TyFun Type Type) = forall (arg :: Type).SameKind (Apply (MatrixTFSym1 ns) arg) (MatrixTFSym2 ns arg) => MatrixTFSym1KindInference
data MatrixTFSym0 (l :: TyFun [Peano] (Type ~> Type)) = forall (arg :: [Peano]).SameKind (Apply MatrixTFSym0 arg) (MatrixTFSym1 arg) => MatrixTFSym0KindInference
eqSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Eq a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Bool
ordSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Ord a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Ordering
compareSingMatrix :: forall (peanos :: [Peano]) (a :: Type) (c :: Type). (a -> a -> c) -> c -> (c -> c -> c) -> Sing peanos -> Matrix peanos a -> Matrix peanos a -> c
fmapSingMatrix :: forall (peanos :: [Peano]) (a :: Type) (b :: Type). Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b
consMatrix :: Matrix ns a -> Matrix (n ': ns) a -> Matrix ('S n ': ns) a
toListMatrix :: forall (peanos :: [Peano]) (a :: Type). Sing peanos -> Matrix peanos a -> [a]
genMatrix :: forall (ns :: [Peano]) (a :: Type). Sing ns -> (HList Fin ns -> a) -> Matrix ns a
genMatrix_ :: SingI ns => (HList Fin ns -> a) -> Matrix ns a
indexMatrix :: HList Fin ns -> Matrix ns a -> a
imapMatrix :: forall (ns :: [Peano]) a b. Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
imapMatrix_ :: SingI ns => (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b
onMatrixTF :: (MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b
onMatrix :: (Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b
updateAtMatrix :: HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a
setAtMatrix :: HList Fin ns -> a -> Matrix ns a -> Matrix ns a

Documentation

data Peano Source #

Constructors

Z
S Peano

Instances

Instances details

Eq Peano Source #
Instance details Defined in Termonad.Config.Vec Methods (==) :: Peano -> Peano -> Bool # (/=) :: Peano -> Peano -> Bool #
Num Peano Source #
Instance details Defined in Termonad.Config.Vec Methods (+) :: Peano -> Peano -> Peano # (-) :: Peano -> Peano -> Peano # (*) :: Peano -> Peano -> Peano # negate :: Peano -> Peano # abs :: Peano -> Peano # signum :: Peano -> Peano # fromInteger :: Integer -> Peano #
Ord Peano Source #
Instance details Defined in Termonad.Config.Vec Methods compare :: Peano -> Peano -> Ordering # (<) :: Peano -> Peano -> Bool # (<=) :: Peano -> Peano -> Bool # (>) :: Peano -> Peano -> Bool # (>=) :: Peano -> Peano -> Bool # max :: Peano -> Peano -> Peano # min :: Peano -> Peano -> Peano #
Show Peano Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> Peano -> ShowS # show :: Peano -> String # showList :: [Peano] -> ShowS #
PShow Peano Source #
Instance details Defined in Termonad.Config.Vec Associated Types type ShowsPrec arg0 arg1 arg2 :: Symbol Source # type Show_ arg0 :: Symbol Source # type ShowList arg0 arg1 :: Symbol Source #
SShow Peano => SShow Peano Source #
Instance details Defined in Termonad.Config.Vec Methods sShowsPrec :: forall (t1 :: Nat) (t2 :: Peano) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) Source # sShow_ :: forall (t :: Peano). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t1 :: [Peano]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) Source #
PNum Peano Source #
Instance details Defined in Termonad.Config.Vec Associated Types type arg0 + arg1 :: a0 Source # type arg0 - arg1 :: a0 Source # type arg0 * arg1 :: a0 Source # type Negate arg0 :: a0 Source # type Abs arg0 :: a0 Source # type Signum arg0 :: a0 Source # type FromInteger arg0 :: a0 Source #
SNum Peano Source #
Instance details Defined in Termonad.Config.Vec Methods (%+) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) Source # (%-) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) Source # (%) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) Source # sNegate :: forall (t :: Peano). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Peano). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Peano). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #
POrd Peano Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Compare arg0 arg1 :: Ordering Source # type arg0 < arg1 :: Bool Source # type arg0 <= arg1 :: Bool Source # type arg0 > arg1 :: Bool Source # type arg0 >= arg1 :: Bool Source # type Max arg0 arg1 :: a0 Source # type Min arg0 arg1 :: a0 Source #
SOrd Peano => SOrd Peano Source #
Instance details Defined in Termonad.Config.Vec Methods sCompare :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) Source # (%<) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) Source # (%<=) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) Source # (%>) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) Source # (%>=) :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) Source # sMax :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) Source # sMin :: forall (t1 :: Peano) (t2 :: Peano). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) Source #
SEq Peano => SEq Peano Source #
Instance details Defined in Termonad.Config.Vec Methods (%==) :: forall (a :: Peano) (b :: Peano). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Peano) (b :: Peano). Sing a -> Sing b -> Sing (a /= b) Source #
PEq Peano Source #
Instance details Defined in Termonad.Config.Vec Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SDecide Peano => SDecide Peano Source #
Instance details Defined in Termonad.Config.Vec Methods (%~) :: forall (a :: Peano) (b :: Peano). Sing a -> Sing b -> Decision (a :~: b) Source #
SingKind Peano Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Demote Peano = (r :: Type) Source # Methods fromSing :: forall (a :: Peano). Sing a -> Demote Peano Source # toSing :: Demote Peano -> SomeSing Peano Source #
SingI 'Z Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing 'Z Source #
SDecide Peano => TestEquality SPeano Source #
Instance details Defined in Termonad.Config.Vec Methods testEquality :: forall (a :: k) (b :: k). SPeano a -> SPeano b -> Maybe (a :~: b)
SDecide Peano => TestCoercion SPeano Source #
Instance details Defined in Termonad.Config.Vec Methods testCoercion :: forall (a :: k) (b :: k). SPeano a -> SPeano b -> Maybe (Coercion a b)
SingI n => SingI ('S n :: Peano) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing ('S n) Source #
Num a => Num (Matrix ('[] :: [Peano]) a) Source #
Instance details Defined in Termonad.Config.Vec Methods (+) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # (-) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # (*) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # negate :: Matrix '[] a -> Matrix '[] a # abs :: Matrix '[] a -> Matrix '[] a # signum :: Matrix '[] a -> Matrix '[] a # fromInteger :: Integer -> Matrix '[] a #
SuppressUnusedWarnings FromInteger_6989586621679478536Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings ShowsPrec_6989586621679477933Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings Signum_6989586621679478530Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings Abs_6989586621679478521Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings Compare_6989586621679477240Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings TFHelper_6989586621679478506Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings TFHelper_6989586621679478490Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings TFHelper_6989586621679478474Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings AddPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings SubtractPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings MultPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI SSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing SSym0 Source #
SingI AddPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing AddPeanoSym0 Source #
SingI SubtractPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing SubtractPeanoSym0 Source #
SingI MultPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing MultPeanoSym0 Source #
SuppressUnusedWarnings (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SuppressUnusedWarnings (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (AddPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (AddPeanoSym1 d) Source #
SingI d => SingI (SubtractPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (SubtractPeanoSym1 d) Source #
SingI d => SingI (MultPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (MultPeanoSym1 d) Source #
type Sing Source #
Instance details Defined in Termonad.Config.Vec type Sing = SPeano
type Demote Peano Source #
Instance details Defined in Termonad.Config.Vec type Demote Peano = Peano
type Show_ (arg0 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Show_ (arg0 :: Peano) = Apply (Show__6989586621680577850Sym0 :: TyFun Peano Symbol -> Type) arg0
type FromInteger a Source #
Instance details Defined in Termonad.Config.Vec type FromInteger a = Apply FromInteger_6989586621679478536Sym0 a
type Signum (a :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Signum (a :: Peano) = Apply Signum_6989586621679478530Sym0 a
type Abs (a :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Abs (a :: Peano) = Apply Abs_6989586621679478521Sym0 a
type Negate (arg0 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Negate (arg0 :: Peano) = Apply (Negate_6989586621679927739Sym0 :: TyFun Peano Peano -> Type) arg0
type ShowList (arg0 :: [Peano]) arg1 Source #
Instance details Defined in Termonad.Config.Vec type ShowList (arg0 :: [Peano]) arg1 = Apply (Apply (ShowList_6989586621680577858Sym0 :: TyFun [Peano] (Symbol ~> Symbol) -> Type) arg0) arg1
type (a1 :: Peano) * (a2 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (a1 :: Peano) * (a2 :: Peano) = Apply (Apply TFHelper_6989586621679478506Sym0 a1) a2
type (a1 :: Peano) - (a2 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (a1 :: Peano) - (a2 :: Peano) = Apply (Apply TFHelper_6989586621679478490Sym0 a1) a2
type (a1 :: Peano) + (a2 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (a1 :: Peano) + (a2 :: Peano) = Apply (Apply TFHelper_6989586621679478474Sym0 a1) a2
type Min (arg0 :: Peano) (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Min (arg0 :: Peano) (arg1 :: Peano) = Apply (Apply (Min_6989586621679792618Sym0 :: TyFun Peano (Peano ~> Peano) -> Type) arg0) arg1
type Max (arg0 :: Peano) (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Max (arg0 :: Peano) (arg1 :: Peano) = Apply (Apply (Max_6989586621679792600Sym0 :: TyFun Peano (Peano ~> Peano) -> Type) arg0) arg1
type (arg0 :: Peano) >= (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (arg0 :: Peano) >= (arg1 :: Peano) = Apply (Apply (TFHelper_6989586621679792582Sym0 :: TyFun Peano (Peano ~> Bool) -> Type) arg0) arg1
type (arg0 :: Peano) > (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (arg0 :: Peano) > (arg1 :: Peano) = Apply (Apply (TFHelper_6989586621679792564Sym0 :: TyFun Peano (Peano ~> Bool) -> Type) arg0) arg1
type (arg0 :: Peano) <= (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (arg0 :: Peano) <= (arg1 :: Peano) = Apply (Apply (TFHelper_6989586621679792546Sym0 :: TyFun Peano (Peano ~> Bool) -> Type) arg0) arg1
type (arg0 :: Peano) < (arg1 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (arg0 :: Peano) < (arg1 :: Peano) = Apply (Apply (TFHelper_6989586621679792528Sym0 :: TyFun Peano (Peano ~> Bool) -> Type) arg0) arg1
type Compare (a1 :: Peano) (a2 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Compare (a1 :: Peano) (a2 :: Peano) = Apply (Apply Compare_6989586621679477240Sym0 a1) a2
type (x :: Peano) /= (y :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (x :: Peano) /= (y :: Peano) = Not (x == y)
type (a :: Peano) == (b :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type (a :: Peano) == (b :: Peano) = Equals_6989586621679478552 a b
type ShowsPrec a1 (a2 :: Peano) a3 Source #
Instance details Defined in Termonad.Config.Vec type ShowsPrec a1 (a2 :: Peano) a3 = Apply (Apply (Apply ShowsPrec_6989586621679477933Sym0 a1) a2) a3
type Apply FromInteger_6989586621679478536Sym0 (a6989586621679478535 :: Nat) Source #
Instance details Defined in Termonad.Config.Vec type Apply FromInteger_6989586621679478536Sym0 (a6989586621679478535 :: Nat) = FromInteger_6989586621679478536 a6989586621679478535
type Apply Signum_6989586621679478530Sym0 (a6989586621679478529 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Signum_6989586621679478530Sym0 (a6989586621679478529 :: Peano) = Signum_6989586621679478530 a6989586621679478529
type Apply Abs_6989586621679478521Sym0 (a6989586621679478520 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Abs_6989586621679478521Sym0 (a6989586621679478520 :: Peano) = Abs_6989586621679478521 a6989586621679478520
type Apply SSym0 (t6989586621679475479 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply SSym0 (t6989586621679475479 :: Peano) = 'S t6989586621679475479
type Apply (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) (a6989586621679477239 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) (a6989586621679477239 :: Peano) = Compare_6989586621679477240 a6989586621679477238 a6989586621679477239
type Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) (a6989586621679478505 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) (a6989586621679478505 :: Peano) = TFHelper_6989586621679478506 a6989586621679478504 a6989586621679478505
type Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) (a6989586621679478489 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) (a6989586621679478489 :: Peano) = TFHelper_6989586621679478490 a6989586621679478488 a6989586621679478489
type Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) (a6989586621679478473 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) (a6989586621679478473 :: Peano) = TFHelper_6989586621679478474 a6989586621679478472 a6989586621679478473
type Apply (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) (a6989586621679475495 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) (a6989586621679475495 :: Peano) = AddPeano a6989586621679475494 a6989586621679475495
type Apply (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) (a6989586621679475488 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) (a6989586621679475488 :: Peano) = SubtractPeano a6989586621679475487 a6989586621679475488
type Apply (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) (a6989586621679475482 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) (a6989586621679475482 :: Peano) = MultPeano a6989586621679475481 a6989586621679475482
type Apply ShowsPrec_6989586621679477933Sym0 (a6989586621679477930 :: Nat) Source #
Instance details Defined in Termonad.Config.Vec type Apply ShowsPrec_6989586621679477933Sym0 (a6989586621679477930 :: Nat) = ShowsPrec_6989586621679477933Sym1 a6989586621679477930
type Apply Compare_6989586621679477240Sym0 (a6989586621679477238 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Compare_6989586621679477240Sym0 (a6989586621679477238 :: Peano) = Compare_6989586621679477240Sym1 a6989586621679477238
type Apply TFHelper_6989586621679478506Sym0 (a6989586621679478504 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478506Sym0 (a6989586621679478504 :: Peano) = TFHelper_6989586621679478506Sym1 a6989586621679478504
type Apply TFHelper_6989586621679478490Sym0 (a6989586621679478488 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478490Sym0 (a6989586621679478488 :: Peano) = TFHelper_6989586621679478490Sym1 a6989586621679478488
type Apply TFHelper_6989586621679478474Sym0 (a6989586621679478472 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478474Sym0 (a6989586621679478472 :: Peano) = TFHelper_6989586621679478474Sym1 a6989586621679478472
type Apply AddPeanoSym0 (a6989586621679475494 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply AddPeanoSym0 (a6989586621679475494 :: Peano) = AddPeanoSym1 a6989586621679475494
type Apply SubtractPeanoSym0 (a6989586621679475487 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply SubtractPeanoSym0 (a6989586621679475487 :: Peano) = SubtractPeanoSym1 a6989586621679475487
type Apply MultPeanoSym0 (a6989586621679475481 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply MultPeanoSym0 (a6989586621679475481 :: Peano) = MultPeanoSym1 a6989586621679475481
type Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679477931 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679477931 :: Peano) = ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931
type Apply MatrixTFSym0 (l :: [Peano]) Source #
Instance details Defined in Termonad.Config.Vec type Apply MatrixTFSym0 (l :: [Peano]) = MatrixTFSym1 l

type ZSym0 = Z Source #

type SSym1 (t6989586621679475479 :: Peano) = S t6989586621679475479 Source #

data SSym0 :: (~>) Peano Peano where Source #

Constructors

SSym0KindInference :: forall t6989586621679475479 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679475479

Instances

Instances details

SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI SSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing SSym0 Source #
type Apply SSym0 (t6989586621679475479 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply SSym0 (t6989586621679475479 :: Peano) = 'S t6989586621679475479

type family N0 :: Peano where ... Source #

Equations

N0 = ZSym0

type N0Sym0 = N0 Source #

type family N1 :: Peano where ... Source #

Equations

N1 = Apply SSym0 N0Sym0

type N1Sym0 = N1 Source #

type family N2 :: Peano where ... Source #

Equations

N2 = Apply SSym0 N1Sym0

type N2Sym0 = N2 Source #

type family N3 :: Peano where ... Source #

Equations

N3 = Apply SSym0 N2Sym0

type N3Sym0 = N3 Source #

type family N4 :: Peano where ... Source #

Equations

N4 = Apply SSym0 N3Sym0

type N4Sym0 = N4 Source #

type family N5 :: Peano where ... Source #

Equations

N5 = Apply SSym0 N4Sym0

type N5Sym0 = N5 Source #

type family N6 :: Peano where ... Source #

Equations

N6 = Apply SSym0 N5Sym0

type N6Sym0 = N6 Source #

type family N7 :: Peano where ... Source #

Equations

N7 = Apply SSym0 N6Sym0

type N7Sym0 = N7 Source #

type family N8 :: Peano where ... Source #

Equations

N8 = Apply SSym0 N7Sym0

type N8Sym0 = N8 Source #

type family N9 :: Peano where ... Source #

Equations

N9 = Apply SSym0 N8Sym0

type N9Sym0 = N9 Source #

type family N10 :: Peano where ... Source #

Equations

N10 = Apply SSym0 N9Sym0

type N10Sym0 = N10 Source #

type family SubtractPeano (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

SubtractPeano Z _ = ZSym0
SubtractPeano a Z = a
SubtractPeano (S a) (S b) = Apply (Apply SubtractPeanoSym0 a) b

data SubtractPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

SubtractPeanoSym0KindInference :: forall a6989586621679475487 arg. SameKind (Apply SubtractPeanoSym0 arg) (SubtractPeanoSym1 arg) => SubtractPeanoSym0 a6989586621679475487

Instances

Instances details

SuppressUnusedWarnings SubtractPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI SubtractPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing SubtractPeanoSym0 Source #
type Apply SubtractPeanoSym0 (a6989586621679475487 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply SubtractPeanoSym0 (a6989586621679475487 :: Peano) = SubtractPeanoSym1 a6989586621679475487

data SubtractPeanoSym1 (a6989586621679475487 :: Peano) :: (~>) Peano Peano where Source #

Constructors

SubtractPeanoSym1KindInference :: forall a6989586621679475487 a6989586621679475488 arg. SameKind (Apply (SubtractPeanoSym1 a6989586621679475487) arg) (SubtractPeanoSym2 a6989586621679475487 arg) => SubtractPeanoSym1 a6989586621679475487 a6989586621679475488

Instances

Instances details

SuppressUnusedWarnings (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (SubtractPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (SubtractPeanoSym1 d) Source #
type Apply (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) (a6989586621679475488 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (SubtractPeanoSym1 a6989586621679475487 :: TyFun Peano Peano -> Type) (a6989586621679475488 :: Peano) = SubtractPeano a6989586621679475487 a6989586621679475488

type SubtractPeanoSym2 (a6989586621679475487 :: Peano) (a6989586621679475488 :: Peano) = SubtractPeano a6989586621679475487 a6989586621679475488 Source #

type family AddPeano (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

AddPeano Z a = a
AddPeano (S a) b = Apply SSym0 (Apply (Apply AddPeanoSym0 a) b)

data AddPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

AddPeanoSym0KindInference :: forall a6989586621679475494 arg. SameKind (Apply AddPeanoSym0 arg) (AddPeanoSym1 arg) => AddPeanoSym0 a6989586621679475494

Instances

Instances details

SuppressUnusedWarnings AddPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI AddPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing AddPeanoSym0 Source #
type Apply AddPeanoSym0 (a6989586621679475494 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply AddPeanoSym0 (a6989586621679475494 :: Peano) = AddPeanoSym1 a6989586621679475494

data AddPeanoSym1 (a6989586621679475494 :: Peano) :: (~>) Peano Peano where Source #

Constructors

AddPeanoSym1KindInference :: forall a6989586621679475494 a6989586621679475495 arg. SameKind (Apply (AddPeanoSym1 a6989586621679475494) arg) (AddPeanoSym2 a6989586621679475494 arg) => AddPeanoSym1 a6989586621679475494 a6989586621679475495

Instances

Instances details

SuppressUnusedWarnings (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (AddPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (AddPeanoSym1 d) Source #
type Apply (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) (a6989586621679475495 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (AddPeanoSym1 a6989586621679475494 :: TyFun Peano Peano -> Type) (a6989586621679475495 :: Peano) = AddPeano a6989586621679475494 a6989586621679475495

type AddPeanoSym2 (a6989586621679475494 :: Peano) (a6989586621679475495 :: Peano) = AddPeano a6989586621679475494 a6989586621679475495 Source #

type family MultPeano (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

MultPeano Z _ = ZSym0
MultPeano (S a) b = Apply (Apply AddPeanoSym0 (Apply (Apply MultPeanoSym0 a) b)) b

data MultPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

MultPeanoSym0KindInference :: forall a6989586621679475481 arg. SameKind (Apply MultPeanoSym0 arg) (MultPeanoSym1 arg) => MultPeanoSym0 a6989586621679475481

Instances

Instances details

SuppressUnusedWarnings MultPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI MultPeanoSym0 Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing MultPeanoSym0 Source #
type Apply MultPeanoSym0 (a6989586621679475481 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply MultPeanoSym0 (a6989586621679475481 :: Peano) = MultPeanoSym1 a6989586621679475481

data MultPeanoSym1 (a6989586621679475481 :: Peano) :: (~>) Peano Peano where Source #

Constructors

MultPeanoSym1KindInference :: forall a6989586621679475481 a6989586621679475482 arg. SameKind (Apply (MultPeanoSym1 a6989586621679475481) arg) (MultPeanoSym2 a6989586621679475481 arg) => MultPeanoSym1 a6989586621679475481 a6989586621679475482

Instances

Instances details

SuppressUnusedWarnings (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
SingI d => SingI (MultPeanoSym1 d :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing (MultPeanoSym1 d) Source #
type Apply (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) (a6989586621679475482 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (MultPeanoSym1 a6989586621679475481 :: TyFun Peano Peano -> Type) (a6989586621679475482 :: Peano) = MultPeano a6989586621679475481 a6989586621679475482

type MultPeanoSym2 (a6989586621679475481 :: Peano) (a6989586621679475482 :: Peano) = MultPeano a6989586621679475481 a6989586621679475482 Source #

type family N24 :: Peano where ... Source #

Equations

N24 = Apply (Apply MultPeanoSym0 N4Sym0) N6Sym0

type N24Sym0 = N24 Source #

type family Compare_6989586621679477240 (a :: Peano) (a :: Peano) :: Ordering where ... Source #

Equations

Compare_6989586621679477240 Z Z = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_6989586621679477240 (S a_6989586621679475469) (S b_6989586621679475471) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_6989586621679475469) b_6989586621679475471)) '[])
Compare_6989586621679477240 Z (S _) = LTSym0
Compare_6989586621679477240 (S _) Z = GTSym0

type Compare_6989586621679477240Sym2 (a6989586621679477238 :: Peano) (a6989586621679477239 :: Peano) = Compare_6989586621679477240 a6989586621679477238 a6989586621679477239 Source #

data Compare_6989586621679477240Sym1 (a6989586621679477238 :: Peano) :: (~>) Peano Ordering where Source #

Constructors

Compare_6989586621679477240Sym1KindInference :: forall a6989586621679477238 a6989586621679477239 arg. SameKind (Apply (Compare_6989586621679477240Sym1 a6989586621679477238) arg) (Compare_6989586621679477240Sym2 a6989586621679477238 arg) => Compare_6989586621679477240Sym1 a6989586621679477238 a6989586621679477239

Instances

Instances details

SuppressUnusedWarnings (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) (a6989586621679477239 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (Compare_6989586621679477240Sym1 a6989586621679477238 :: TyFun Peano Ordering -> Type) (a6989586621679477239 :: Peano) = Compare_6989586621679477240 a6989586621679477238 a6989586621679477239

data Compare_6989586621679477240Sym0 :: (~>) Peano ((~>) Peano Ordering) where Source #

Constructors

Compare_6989586621679477240Sym0KindInference :: forall a6989586621679477238 arg. SameKind (Apply Compare_6989586621679477240Sym0 arg) (Compare_6989586621679477240Sym1 arg) => Compare_6989586621679477240Sym0 a6989586621679477238

Instances

Instances details

SuppressUnusedWarnings Compare_6989586621679477240Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply Compare_6989586621679477240Sym0 (a6989586621679477238 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Compare_6989586621679477240Sym0 (a6989586621679477238 :: Peano) = Compare_6989586621679477240Sym1 a6989586621679477238

type family ShowsPrec_6989586621679477933 (a :: Nat) (a :: Peano) (a :: Symbol) :: Symbol where ... Source #

Equations

ShowsPrec_6989586621679477933 _ Z a_6989586621679477941 = Apply (Apply ShowStringSym0 (FromString "Z")) a_6989586621679477941
ShowsPrec_6989586621679477933 p_6989586621679475473 (S arg_6989586621679475475) a_6989586621679477943 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_6989586621679475473) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 (FromString "S "))) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_6989586621679475475))) a_6989586621679477943

type ShowsPrec_6989586621679477933Sym3 (a6989586621679477930 :: Nat) (a6989586621679477931 :: Peano) (a6989586621679477932 :: Symbol) = ShowsPrec_6989586621679477933 a6989586621679477930 a6989586621679477931 a6989586621679477932 Source #

data ShowsPrec_6989586621679477933Sym2 (a6989586621679477930 :: Nat) (a6989586621679477931 :: Peano) :: (~>) Symbol Symbol where Source #

Constructors

ShowsPrec_6989586621679477933Sym2KindInference :: forall a6989586621679477930 a6989586621679477931 a6989586621679477932 arg. SameKind (Apply (ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931) arg) (ShowsPrec_6989586621679477933Sym3 a6989586621679477930 a6989586621679477931 arg) => ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931 a6989586621679477932

Instances

Instances details

SuppressUnusedWarnings (ShowsPrec_6989586621679477933Sym2 a6989586621679477931 a6989586621679477930 :: TyFun Symbol Symbol -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (ShowsPrec_6989586621679477933Sym2 a6989586621679477931 a6989586621679477930 :: TyFun Symbol Symbol -> Type) (a6989586621679477932 :: Symbol) Source #
Instance details Defined in Termonad.Config.Vec type Apply (ShowsPrec_6989586621679477933Sym2 a6989586621679477931 a6989586621679477930 :: TyFun Symbol Symbol -> Type) (a6989586621679477932 :: Symbol) = ShowsPrec_6989586621679477933 a6989586621679477931 a6989586621679477930 a6989586621679477932

data ShowsPrec_6989586621679477933Sym1 (a6989586621679477930 :: Nat) :: (~>) Peano ((~>) Symbol Symbol) where Source #

Constructors

ShowsPrec_6989586621679477933Sym1KindInference :: forall a6989586621679477930 a6989586621679477931 arg. SameKind (Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930) arg) (ShowsPrec_6989586621679477933Sym2 a6989586621679477930 arg) => ShowsPrec_6989586621679477933Sym1 a6989586621679477930 a6989586621679477931

Instances

Instances details

SuppressUnusedWarnings (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679477931 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (ShowsPrec_6989586621679477933Sym1 a6989586621679477930 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679477931 :: Peano) = ShowsPrec_6989586621679477933Sym2 a6989586621679477930 a6989586621679477931

data ShowsPrec_6989586621679477933Sym0 :: (~>) Nat ((~>) Peano ((~>) Symbol Symbol)) where Source #

Constructors

ShowsPrec_6989586621679477933Sym0KindInference :: forall a6989586621679477930 arg. SameKind (Apply ShowsPrec_6989586621679477933Sym0 arg) (ShowsPrec_6989586621679477933Sym1 arg) => ShowsPrec_6989586621679477933Sym0 a6989586621679477930

Instances

Instances details

SuppressUnusedWarnings ShowsPrec_6989586621679477933Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply ShowsPrec_6989586621679477933Sym0 (a6989586621679477930 :: Nat) Source #
Instance details Defined in Termonad.Config.Vec type Apply ShowsPrec_6989586621679477933Sym0 (a6989586621679477930 :: Nat) = ShowsPrec_6989586621679477933Sym1 a6989586621679477930

type family TFHelper_6989586621679478474 (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

TFHelper_6989586621679478474 a_6989586621679478476 a_6989586621679478478 = Apply (Apply AddPeanoSym0 a_6989586621679478476) a_6989586621679478478

type TFHelper_6989586621679478474Sym2 (a6989586621679478472 :: Peano) (a6989586621679478473 :: Peano) = TFHelper_6989586621679478474 a6989586621679478472 a6989586621679478473 Source #

data TFHelper_6989586621679478474Sym1 (a6989586621679478472 :: Peano) :: (~>) Peano Peano where Source #

Constructors

TFHelper_6989586621679478474Sym1KindInference :: forall a6989586621679478472 a6989586621679478473 arg. SameKind (Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472) arg) (TFHelper_6989586621679478474Sym2 a6989586621679478472 arg) => TFHelper_6989586621679478474Sym1 a6989586621679478472 a6989586621679478473

Instances

Instances details

SuppressUnusedWarnings (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) (a6989586621679478473 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478474Sym1 a6989586621679478472 :: TyFun Peano Peano -> Type) (a6989586621679478473 :: Peano) = TFHelper_6989586621679478474 a6989586621679478472 a6989586621679478473

data TFHelper_6989586621679478474Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

TFHelper_6989586621679478474Sym0KindInference :: forall a6989586621679478472 arg. SameKind (Apply TFHelper_6989586621679478474Sym0 arg) (TFHelper_6989586621679478474Sym1 arg) => TFHelper_6989586621679478474Sym0 a6989586621679478472

Instances

Instances details

SuppressUnusedWarnings TFHelper_6989586621679478474Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply TFHelper_6989586621679478474Sym0 (a6989586621679478472 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478474Sym0 (a6989586621679478472 :: Peano) = TFHelper_6989586621679478474Sym1 a6989586621679478472

type family TFHelper_6989586621679478490 (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

TFHelper_6989586621679478490 a_6989586621679478492 a_6989586621679478494 = Apply (Apply SubtractPeanoSym0 a_6989586621679478492) a_6989586621679478494

type TFHelper_6989586621679478490Sym2 (a6989586621679478488 :: Peano) (a6989586621679478489 :: Peano) = TFHelper_6989586621679478490 a6989586621679478488 a6989586621679478489 Source #

data TFHelper_6989586621679478490Sym1 (a6989586621679478488 :: Peano) :: (~>) Peano Peano where Source #

Constructors

TFHelper_6989586621679478490Sym1KindInference :: forall a6989586621679478488 a6989586621679478489 arg. SameKind (Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488) arg) (TFHelper_6989586621679478490Sym2 a6989586621679478488 arg) => TFHelper_6989586621679478490Sym1 a6989586621679478488 a6989586621679478489

Instances

Instances details

SuppressUnusedWarnings (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) (a6989586621679478489 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478490Sym1 a6989586621679478488 :: TyFun Peano Peano -> Type) (a6989586621679478489 :: Peano) = TFHelper_6989586621679478490 a6989586621679478488 a6989586621679478489

data TFHelper_6989586621679478490Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

TFHelper_6989586621679478490Sym0KindInference :: forall a6989586621679478488 arg. SameKind (Apply TFHelper_6989586621679478490Sym0 arg) (TFHelper_6989586621679478490Sym1 arg) => TFHelper_6989586621679478490Sym0 a6989586621679478488

Instances

Instances details

SuppressUnusedWarnings TFHelper_6989586621679478490Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply TFHelper_6989586621679478490Sym0 (a6989586621679478488 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478490Sym0 (a6989586621679478488 :: Peano) = TFHelper_6989586621679478490Sym1 a6989586621679478488

type family TFHelper_6989586621679478506 (a :: Peano) (a :: Peano) :: Peano where ... Source #

Equations

TFHelper_6989586621679478506 a_6989586621679478508 a_6989586621679478510 = Apply (Apply MultPeanoSym0 a_6989586621679478508) a_6989586621679478510

type TFHelper_6989586621679478506Sym2 (a6989586621679478504 :: Peano) (a6989586621679478505 :: Peano) = TFHelper_6989586621679478506 a6989586621679478504 a6989586621679478505 Source #

data TFHelper_6989586621679478506Sym1 (a6989586621679478504 :: Peano) :: (~>) Peano Peano where Source #

Constructors

TFHelper_6989586621679478506Sym1KindInference :: forall a6989586621679478504 a6989586621679478505 arg. SameKind (Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504) arg) (TFHelper_6989586621679478506Sym2 a6989586621679478504 arg) => TFHelper_6989586621679478506Sym1 a6989586621679478504 a6989586621679478505

Instances

Instances details

SuppressUnusedWarnings (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) (a6989586621679478505 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679478506Sym1 a6989586621679478504 :: TyFun Peano Peano -> Type) (a6989586621679478505 :: Peano) = TFHelper_6989586621679478506 a6989586621679478504 a6989586621679478505

data TFHelper_6989586621679478506Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #

Constructors

TFHelper_6989586621679478506Sym0KindInference :: forall a6989586621679478504 arg. SameKind (Apply TFHelper_6989586621679478506Sym0 arg) (TFHelper_6989586621679478506Sym1 arg) => TFHelper_6989586621679478506Sym0 a6989586621679478504

Instances

Instances details

SuppressUnusedWarnings TFHelper_6989586621679478506Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply TFHelper_6989586621679478506Sym0 (a6989586621679478504 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679478506Sym0 (a6989586621679478504 :: Peano) = TFHelper_6989586621679478506Sym1 a6989586621679478504

type family Abs_6989586621679478521 (a :: Peano) :: Peano where ... Source #

Equations

Abs_6989586621679478521 a_6989586621679478523 = Apply IdSym0 a_6989586621679478523

type Abs_6989586621679478521Sym1 (a6989586621679478520 :: Peano) = Abs_6989586621679478521 a6989586621679478520 Source #

data Abs_6989586621679478521Sym0 :: (~>) Peano Peano where Source #

Constructors

Abs_6989586621679478521Sym0KindInference :: forall a6989586621679478520 arg. SameKind (Apply Abs_6989586621679478521Sym0 arg) (Abs_6989586621679478521Sym1 arg) => Abs_6989586621679478521Sym0 a6989586621679478520

Instances

Instances details

SuppressUnusedWarnings Abs_6989586621679478521Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply Abs_6989586621679478521Sym0 (a6989586621679478520 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Abs_6989586621679478521Sym0 (a6989586621679478520 :: Peano) = Abs_6989586621679478521 a6989586621679478520

type family Signum_6989586621679478530 (a :: Peano) :: Peano where ... Source #

Equations

Signum_6989586621679478530 Z = ZSym0
Signum_6989586621679478530 (S _) = Apply SSym0 ZSym0

type Signum_6989586621679478530Sym1 (a6989586621679478529 :: Peano) = Signum_6989586621679478530 a6989586621679478529 Source #

data Signum_6989586621679478530Sym0 :: (~>) Peano Peano where Source #

Constructors

Signum_6989586621679478530Sym0KindInference :: forall a6989586621679478529 arg. SameKind (Apply Signum_6989586621679478530Sym0 arg) (Signum_6989586621679478530Sym1 arg) => Signum_6989586621679478530Sym0 a6989586621679478529

Instances

Instances details

SuppressUnusedWarnings Signum_6989586621679478530Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply Signum_6989586621679478530Sym0 (a6989586621679478529 :: Peano) Source #
Instance details Defined in Termonad.Config.Vec type Apply Signum_6989586621679478530Sym0 (a6989586621679478529 :: Peano) = Signum_6989586621679478530 a6989586621679478529

type family Let6989586621679478541Scrutinee_6989586621679463510 n where ... Source #

Equations

Let6989586621679478541Scrutinee_6989586621679463510 n = Apply (Apply (<@#@$) n) (FromInteger 0)

type Let6989586621679478541Scrutinee_6989586621679463510Sym1 n6989586621679478540 = Let6989586621679478541Scrutinee_6989586621679463510 n6989586621679478540 Source #

data Let6989586621679478541Scrutinee_6989586621679463510Sym0 n6989586621679478540 where Source #

Constructors

Let6989586621679478541Scrutinee_6989586621679463510Sym0KindInference :: forall n6989586621679478540 arg. SameKind (Apply Let6989586621679478541Scrutinee_6989586621679463510Sym0 arg) (Let6989586621679478541Scrutinee_6989586621679463510Sym1 arg) => Let6989586621679478541Scrutinee_6989586621679463510Sym0 n6989586621679478540

Instances

Instances details

SuppressUnusedWarnings (Let6989586621679478541Scrutinee_6989586621679463510Sym0 :: TyFun k1 Bool -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (Let6989586621679478541Scrutinee_6989586621679463510Sym0 :: TyFun k1 Bool -> Type) (n6989586621679478540 :: k1) Source #
Instance details Defined in Termonad.Config.Vec type Apply (Let6989586621679478541Scrutinee_6989586621679463510Sym0 :: TyFun k1 Bool -> Type) (n6989586621679478540 :: k1) = Let6989586621679478541Scrutinee_6989586621679463510 n6989586621679478540

type family Let6989586621679478545Scrutinee_6989586621679463512 n where ... Source #

Equations

Let6989586621679478545Scrutinee_6989586621679463512 n = Apply (Apply (==@#@$) n) (FromInteger 0)

type Let6989586621679478545Scrutinee_6989586621679463512Sym1 n6989586621679478540 = Let6989586621679478545Scrutinee_6989586621679463512 n6989586621679478540 Source #

data Let6989586621679478545Scrutinee_6989586621679463512Sym0 n6989586621679478540 where Source #

Constructors

Let6989586621679478545Scrutinee_6989586621679463512Sym0KindInference :: forall n6989586621679478540 arg. SameKind (Apply Let6989586621679478545Scrutinee_6989586621679463512Sym0 arg) (Let6989586621679478545Scrutinee_6989586621679463512Sym1 arg) => Let6989586621679478545Scrutinee_6989586621679463512Sym0 n6989586621679478540

Instances

Instances details

SuppressUnusedWarnings (Let6989586621679478545Scrutinee_6989586621679463512Sym0 :: TyFun k1 Bool -> Type) Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply (Let6989586621679478545Scrutinee_6989586621679463512Sym0 :: TyFun k1 Bool -> Type) (n6989586621679478540 :: k1) Source #
Instance details Defined in Termonad.Config.Vec type Apply (Let6989586621679478545Scrutinee_6989586621679463512Sym0 :: TyFun k1 Bool -> Type) (n6989586621679478540 :: k1) = Let6989586621679478545Scrutinee_6989586621679463512 n6989586621679478540

type family Case_6989586621679478547 n t where ... Source #

Equations

Case_6989586621679478547 n 'True = ZSym0
Case_6989586621679478547 n 'False = Apply SSym0 (Apply FromIntegerSym0 (Apply (Apply (-@#@$) n) (FromInteger 1)))

type family Case_6989586621679478543 n t where ... Source #

Equations

Case_6989586621679478543 n 'True = Apply ErrorSym0 (FromString "Num Peano fromInteger: n is negative")
Case_6989586621679478543 n 'False = Case_6989586621679478547 n (Let6989586621679478545Scrutinee_6989586621679463512Sym1 n)

type family FromInteger_6989586621679478536 (a :: Nat) :: Peano where ... Source #

Equations

FromInteger_6989586621679478536 n = Case_6989586621679478543 n (Let6989586621679478541Scrutinee_6989586621679463510Sym1 n)

type FromInteger_6989586621679478536Sym1 (a6989586621679478535 :: Nat) = FromInteger_6989586621679478536 a6989586621679478535 Source #

data FromInteger_6989586621679478536Sym0 :: (~>) Nat Peano where Source #

Constructors

FromInteger_6989586621679478536Sym0KindInference :: forall a6989586621679478535 arg. SameKind (Apply FromInteger_6989586621679478536Sym0 arg) (FromInteger_6989586621679478536Sym1 arg) => FromInteger_6989586621679478536Sym0 a6989586621679478535

Instances

Instances details

SuppressUnusedWarnings FromInteger_6989586621679478536Sym0 Source #
Instance details Defined in Termonad.Config.Vec Methods suppressUnusedWarnings :: () Source #
type Apply FromInteger_6989586621679478536Sym0 (a6989586621679478535 :: Nat) Source #
Instance details Defined in Termonad.Config.Vec type Apply FromInteger_6989586621679478536Sym0 (a6989586621679478535 :: Nat) = FromInteger_6989586621679478536 a6989586621679478535

type family Equals_6989586621679478552 (a :: Peano) (b :: Peano) :: Bool where ... Source #

Equations

Equals_6989586621679478552 Z Z = TrueSym0
Equals_6989586621679478552 (S a) (S b) = (==) a b
Equals_6989586621679478552 (_ :: Peano) (_ :: Peano) = FalseSym0

data SPeano :: Peano -> Type where Source #

Constructors

SZ :: SPeano Z
SS :: forall (n :: Peano). (Sing (n :: Peano)) -> SPeano (S n)

Instances

Instances details

SDecide Peano => TestEquality SPeano Source #
Instance details Defined in Termonad.Config.Vec Methods testEquality :: forall (a :: k) (b :: k). SPeano a -> SPeano b -> Maybe (a :~: b)
SDecide Peano => TestCoercion SPeano Source #
Instance details Defined in Termonad.Config.Vec Methods testCoercion :: forall (a :: k) (b :: k). SPeano a -> SPeano b -> Maybe (Coercion a b)
ShowSing Peano => Show (SPeano z) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> SPeano z -> ShowS # show :: SPeano z -> String # showList :: [SPeano z] -> ShowS #

sAddPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply AddPeanoSym0 t) t :: Peano) Source #

sSubtractPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply SubtractPeanoSym0 t) t :: Peano) Source #

sMultPeano :: forall (t :: Peano) (t :: Peano). Sing t -> Sing t -> Sing (Apply (Apply MultPeanoSym0 t) t :: Peano) Source #

sN0 :: Sing (N0Sym0 :: Peano) Source #

sN1 :: Sing (N1Sym0 :: Peano) Source #

sN2 :: Sing (N2Sym0 :: Peano) Source #

sN3 :: Sing (N3Sym0 :: Peano) Source #

sN4 :: Sing (N4Sym0 :: Peano) Source #

sN5 :: Sing (N5Sym0 :: Peano) Source #

sN6 :: Sing (N6Sym0 :: Peano) Source #

sN7 :: Sing (N7Sym0 :: Peano) Source #

sN8 :: Sing (N8Sym0 :: Peano) Source #

sN9 :: Sing (N9Sym0 :: Peano) Source #

sN10 :: Sing (N10Sym0 :: Peano) Source #

sN24 :: Sing (N24Sym0 :: Peano) Source #

n24 :: Peano Source #

n10 :: Peano Source #

n9 :: Peano Source #

n8 :: Peano Source #

n7 :: Peano Source #

n6 :: Peano Source #

n5 :: Peano Source #

n4 :: Peano Source #

n3 :: Peano Source #

n2 :: Peano Source #

n1 :: Peano Source #

n0 :: Peano Source #

multPeano :: Peano -> Peano -> Peano Source #

subtractPeano :: Peano -> Peano -> Peano Source #

addPeano :: Peano -> Peano -> Peano Source #

ltSuccProof :: forall (n :: Peano) (m :: Peano) proxy. ('S n < 'S m) ~ 'True => proxy n -> proxy m -> (n < m) :~: 'True Source #

This is a proof that if we know S n is less than S m, then we know n is also less than m.

>>> ltSuccProof (sing :: Sing N4) (sing :: Sing N5)
Refl

data Fin :: Peano -> Type where Source #

Constructors

FZ :: forall (n :: Peano). Fin ('S n)
FS :: forall (n :: Peano). !(Fin n) -> Fin ('S n)

Instances

Instances details

Eq (Fin n) Source #
Instance details Defined in Termonad.Config.Vec Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
Ord (Fin n) Source #
Instance details Defined in Termonad.Config.Vec Methods compare :: Fin n -> Fin n -> Ordering # (<) :: Fin n -> Fin n -> Bool # (<=) :: Fin n -> Fin n -> Bool # (>) :: Fin n -> Fin n -> Bool # (>=) :: Fin n -> Fin n -> Bool # max :: Fin n -> Fin n -> Fin n # min :: Fin n -> Fin n -> Fin n #
Show (Fin n) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #
SingKind (Fin n) Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Demote (Fin n) = (r :: Type) Source # Methods fromSing :: forall (a :: Fin n). Sing a -> Demote (Fin n) Source # toSing :: Demote (Fin n) -> SomeSing (Fin n) Source #
SingI ('FZ :: Fin ('S n)) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing 'FZ Source #
SingI n2 => SingI ('FS n2 :: Fin ('S n1)) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing ('FS n2) Source #
type Sing Source #
Instance details Defined in Termonad.Config.Vec type Sing = SFin :: Fin n -> Type
type Demote (Fin n) Source #
Instance details Defined in Termonad.Config.Vec type Demote (Fin n) = Fin n

toIntFin :: Fin n -> Int Source #

fin :: forall total n. (n < total) ~ 'True => Sing total -> Sing n -> Fin total Source #

Similar to ifin but for Fin.

>>> fin (sing :: Sing N5) (sing :: Sing N1) :: Fin N5
FS FZ

fin_ :: forall total n. (SingI total, (n < total) ~ 'True) => Sing n -> Fin total Source #

Similar to ifin_ but for Fin.

>>> fin_ @N4 (sing :: Sing N2) :: Fin N4
FS (FS FZ)

data SFin :: forall n. Fin n -> Type where Source #

Constructors

SFZ :: SFin 'FZ
SFS :: SFin n -> SFin ('FS n)

Instances

Instances details

Show (SFin n2) => Show (SFin ('FS n2)) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> SFin ('FS n2) -> ShowS # show :: SFin ('FS n2) -> String # showList :: [SFin ('FS n2)] -> ShowS #
Show (SFin ('FZ :: Fin ('S n))) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> SFin 'FZ -> ShowS # show :: SFin 'FZ -> String # showList :: [SFin 'FZ] -> ShowS #

data IFin :: Peano -> Peano -> Type where Source #

Constructors

IFZ :: forall (n :: Peano). IFin ('S n) 'Z
IFS :: forall (n :: Peano) (m :: Peano). !(IFin n m) -> IFin ('S n) ('S m)

Instances

Instances details

Eq (IFin x y) Source #
Instance details Defined in Termonad.Config.Vec Methods (==) :: IFin x y -> IFin x y -> Bool # (/=) :: IFin x y -> IFin x y -> Bool #
Ord (IFin x y) Source #
Instance details Defined in Termonad.Config.Vec Methods compare :: IFin x y -> IFin x y -> Ordering # (<) :: IFin x y -> IFin x y -> Bool # (<=) :: IFin x y -> IFin x y -> Bool # (>) :: IFin x y -> IFin x y -> Bool # (>=) :: IFin x y -> IFin x y -> Bool # max :: IFin x y -> IFin x y -> IFin x y # min :: IFin x y -> IFin x y -> IFin x y #
Show (IFin x y) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> IFin x y -> ShowS # show :: IFin x y -> String # showList :: [IFin x y] -> ShowS #
SingKind (IFin n m) Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Demote (IFin n m) = (r :: Type) Source # Methods fromSing :: forall (a :: IFin n m). Sing a -> Demote (IFin n m) Source # toSing :: Demote (IFin n m) -> SomeSing (IFin n m) Source #
SingI ('IFZ :: IFin ('S n) 'Z) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing 'IFZ Source #
SingI n2 => SingI ('IFS n2 :: IFin ('S n1) ('S m)) Source #
Instance details Defined in Termonad.Config.Vec Methods sing :: Sing ('IFS n2) Source #
type Sing Source #
Instance details Defined in Termonad.Config.Vec type Sing = SIFin :: IFin n m -> Type
type Demote (IFin n m) Source #
Instance details Defined in Termonad.Config.Vec type Demote (IFin n m) = IFin n m

toFinIFin :: IFin n m -> Fin n Source #

toIntIFin :: IFin n m -> Int Source #

ifin :: forall total n. (n < total) ~ 'True => Sing total -> Sing n -> IFin total n Source #

Create an IFin.

>>> ifin (sing :: Sing N5) (sing :: Sing N2) :: IFin N5 N2
IFS (IFS IFZ)

ifin_ :: forall total n. (SingI total, (n < total) ~ 'True) => Sing n -> IFin total n Source #

Create an IFin, but take the total implicitly.

>>> ifin_ @N5 (sing :: Sing N3) :: IFin N5 N3
IFS (IFS (IFS IFZ))

data SIFin :: forall n m. IFin n m -> Type where Source #

Constructors

SIFZ :: SIFin 'IFZ
SIFS :: SIFin x -> SIFin ('IFS x)

Instances

Instances details

Show (SIFin n2) => Show (SIFin ('IFS n2)) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> SIFin ('IFS n2) -> ShowS # show :: SIFin ('IFS n2) -> String # showList :: [SIFin ('IFS n2)] -> ShowS #
Show (SIFin ('IFZ :: IFin ('S n) 'Z)) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> SIFin 'IFZ -> ShowS # show :: SIFin 'IFZ -> String # showList :: [SIFin 'IFZ] -> ShowS #

data HList :: (k -> Type) -> [k] -> Type where Source #

Constructors

EmptyHList :: HList f '[]
(:<) :: forall (f :: k -> Type) (a :: k) (as :: [k]). f a -> HList f as -> HList f (a ': as) infixr 6

pattern ConsHList :: (f a :: Type) -> HList f as -> HList f (a ': as) Source #

Data constructor for :<.

data Vec (n :: Peano) :: Type -> Type where Source #

Constructors

EmptyVec :: Vec 'Z a
(:*) :: !a -> !(Vec n a) -> Vec ('S n) a infixr 6

Instances

Instances details

SingI n => Monad (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Methods (>>=) :: Vec n a -> (a -> Vec n b) -> Vec n b # (>>) :: Vec n a -> Vec n b -> Vec n b # return :: a -> Vec n a #
Functor (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Methods fmap :: (a -> b) -> Vec n a -> Vec n b # (<$) :: a -> Vec n b -> Vec n a #
SingI n => Applicative (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Methods pure :: a -> Vec n a # (<>) :: Vec n (a -> b) -> Vec n a -> Vec n b # liftA2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c # (>) :: Vec n a -> Vec n b -> Vec n b # (<*) :: Vec n a -> Vec n b -> Vec n a #
Foldable (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Methods fold :: Monoid m => Vec n m -> m foldMap :: Monoid m => (a -> m) -> Vec n a -> m foldMap' :: Monoid m => (a -> m) -> Vec n a -> m foldr :: (a -> b -> b) -> b -> Vec n a -> b foldr' :: (a -> b -> b) -> b -> Vec n a -> b foldl :: (b -> a -> b) -> b -> Vec n a -> b foldl' :: (b -> a -> b) -> b -> Vec n a -> b foldr1 :: (a -> a -> a) -> Vec n a -> a foldl1 :: (a -> a -> a) -> Vec n a -> a toList :: Vec n a -> [a] null :: Vec n a -> Bool length :: Vec n a -> Int # elem :: Eq a => a -> Vec n a -> Bool maximum :: Ord a => Vec n a -> a minimum :: Ord a => Vec n a -> a sum :: Num a => Vec n a -> a product :: Num a => Vec n a -> a
SingI n => Distributive (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Methods distribute :: Functor f => f (Vec n a) -> Vec n (f a) Source # collect :: Functor f => (a -> Vec n b) -> f a -> Vec n (f b) Source # distributeM :: Monad m => m (Vec n a) -> Vec n (m a) Source # collectM :: Monad m => (a -> Vec n b) -> m a -> Vec n (m b) Source #
SingI n => Representable (Vec n) Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Rep (Vec n) Source # Methods tabulate :: (Rep (Vec n) -> a) -> Vec n a Source # index :: Vec n a -> Rep (Vec n) -> a Source #
Eq a => Eq (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods (==) :: Vec n a -> Vec n a -> Bool # (/=) :: Vec n a -> Vec n a -> Bool #
Ord a => Ord (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods compare :: Vec n a -> Vec n a -> Ordering # (<) :: Vec n a -> Vec n a -> Bool # (<=) :: Vec n a -> Vec n a -> Bool # (>) :: Vec n a -> Vec n a -> Bool # (>=) :: Vec n a -> Vec n a -> Bool # max :: Vec n a -> Vec n a -> Vec n a # min :: Vec n a -> Vec n a -> Vec n a #
Show a => Show (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> Vec n a -> ShowS # show :: Vec n a -> String # showList :: [Vec n a] -> ShowS #
SingI n => MonoPointed (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods opoint :: Element (Vec n a) -> Vec n a Source #
MonoFoldable (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods ofoldMap :: Monoid m => (Element (Vec n a) -> m) -> Vec n a -> m Source # ofoldr :: (Element (Vec n a) -> b -> b) -> b -> Vec n a -> b Source # ofoldl' :: (a0 -> Element (Vec n a) -> a0) -> a0 -> Vec n a -> a0 Source # otoList :: Vec n a -> [Element (Vec n a)] Source # oall :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool Source # oany :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool Source # onull :: Vec n a -> Bool Source # olength :: Vec n a -> Int Source # olength64 :: Vec n a -> Int64 Source # ocompareLength :: Integral i => Vec n a -> i -> Ordering Source # otraverse_ :: Applicative f => (Element (Vec n a) -> f b) -> Vec n a -> f () Source # ofor_ :: Applicative f => Vec n a -> (Element (Vec n a) -> f b) -> f () Source # omapM_ :: Applicative m => (Element (Vec n a) -> m ()) -> Vec n a -> m () Source # oforM_ :: Applicative m => Vec n a -> (Element (Vec n a) -> m ()) -> m () Source # ofoldlM :: Monad m => (a0 -> Element (Vec n a) -> m a0) -> a0 -> Vec n a -> m a0 Source # ofoldMap1Ex :: Semigroup m => (Element (Vec n a) -> m) -> Vec n a -> m Source # ofoldr1Ex :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a)) -> Vec n a -> Element (Vec n a) Source # ofoldl1Ex' :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a)) -> Vec n a -> Element (Vec n a) Source # headEx :: Vec n a -> Element (Vec n a) Source # lastEx :: Vec n a -> Element (Vec n a) Source # unsafeHead :: Vec n a -> Element (Vec n a) Source # unsafeLast :: Vec n a -> Element (Vec n a) Source # maximumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering) -> Vec n a -> Element (Vec n a) Source # minimumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering) -> Vec n a -> Element (Vec n a) Source # oelem :: Element (Vec n a) -> Vec n a -> Bool Source # onotElem :: Element (Vec n a) -> Vec n a -> Bool Source #
MonoFunctor (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec Methods omap :: (Element (Vec n a) -> Element (Vec n a)) -> Vec n a -> Vec n a Source #
type Rep (Vec n) Source #
Instance details Defined in Termonad.Config.Vec type Rep (Vec n) = Fin n
type Element (Vec n a) Source #
Instance details Defined in Termonad.Config.Vec type Element (Vec n a) = a

pattern ConsVec :: (a :: Type) -> Vec n a -> Vec ('S n) a Source #

Data constructor for :*.

genVec_ :: SingI n => (Fin n -> a) -> Vec n a Source #

genVec :: SPeano n -> (Fin n -> a) -> Vec n a Source #

indexVec :: Fin n -> Vec n a -> a Source #

singletonVec :: a -> Vec N1 a Source #

replaceVec :: Sing n -> a -> Vec n a Source #

imapVec :: forall n a b. (Fin n -> a -> b) -> Vec n a -> Vec n b Source #

replaceVec_ :: SingI n => a -> Vec n a Source #

apVec :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

onHeadVec :: (a -> a) -> Vec ('S n) a -> Vec ('S n) a Source #

dropVec :: Sing m -> Vec (m + n) a -> Vec n a Source #

takeVec :: IFin n m -> Vec n a -> Vec m a Source #

updateAtVec :: Fin n -> (a -> a) -> Vec n a -> Vec n a Source #

setAtVec :: Fin n -> a -> Vec n a -> Vec n a Source #

fromListVec :: Sing n -> [a] -> Maybe (Vec n a) Source #

fromListVec_ :: SingI n => [a] -> Maybe (Vec n a) Source #

unsafeFromListVec :: Sing n -> [a] -> Vec n a Source #

unsafeFromListVec_ :: SingI n => [a] -> Vec n a Source #

type family MatrixTF (ns :: [Peano]) (a :: Type) :: Type where ... Source #

Equations

MatrixTF '[] a = a
MatrixTF (n ': ns) a = Vec n (MatrixTF ns a)

newtype Matrix ns a Source #

Constructors

Matrix
Fields unMatrix :: MatrixTF ns a

Instances

Instances details

SingI ns => Monad (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Methods (>>=) :: Matrix ns a -> (a -> Matrix ns b) -> Matrix ns b # (>>) :: Matrix ns a -> Matrix ns b -> Matrix ns b # return :: a -> Matrix ns a #
SingI ns => Functor (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Methods fmap :: (a -> b) -> Matrix ns a -> Matrix ns b # (<$) :: a -> Matrix ns b -> Matrix ns a #
SingI ns => Applicative (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Methods pure :: a -> Matrix ns a # (<>) :: Matrix ns (a -> b) -> Matrix ns a -> Matrix ns b # liftA2 :: (a -> b -> c) -> Matrix ns a -> Matrix ns b -> Matrix ns c # (>) :: Matrix ns a -> Matrix ns b -> Matrix ns b # (<*) :: Matrix ns a -> Matrix ns b -> Matrix ns a #
SingI ns => Foldable (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Methods fold :: Monoid m => Matrix ns m -> m foldMap :: Monoid m => (a -> m) -> Matrix ns a -> m foldMap' :: Monoid m => (a -> m) -> Matrix ns a -> m foldr :: (a -> b -> b) -> b -> Matrix ns a -> b foldr' :: (a -> b -> b) -> b -> Matrix ns a -> b foldl :: (b -> a -> b) -> b -> Matrix ns a -> b foldl' :: (b -> a -> b) -> b -> Matrix ns a -> b foldr1 :: (a -> a -> a) -> Matrix ns a -> a foldl1 :: (a -> a -> a) -> Matrix ns a -> a toList :: Matrix ns a -> [a] null :: Matrix ns a -> Bool length :: Matrix ns a -> Int # elem :: Eq a => a -> Matrix ns a -> Bool maximum :: Ord a => Matrix ns a -> a minimum :: Ord a => Matrix ns a -> a sum :: Num a => Matrix ns a -> a product :: Num a => Matrix ns a -> a
SingI ns => Distributive (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Methods distribute :: Functor f => f (Matrix ns a) -> Matrix ns (f a) Source # collect :: Functor f => (a -> Matrix ns b) -> f a -> Matrix ns (f b) Source # distributeM :: Monad m => m (Matrix ns a) -> Matrix ns (m a) Source # collectM :: Monad m => (a -> Matrix ns b) -> m a -> Matrix ns (m b) Source #
SingI ns => Representable (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec Associated Types type Rep (Matrix ns) Source # Methods tabulate :: (Rep (Matrix ns) -> a) -> Matrix ns a Source # index :: Matrix ns a -> Rep (Matrix ns) -> a Source #
Eq (MatrixTF ns a) => Eq (Matrix ns a) Source #
Instance details Defined in Termonad.Config.Vec Methods (==) :: Matrix ns a -> Matrix ns a -> Bool # (/=) :: Matrix ns a -> Matrix ns a -> Bool #
Num a => Num (Matrix ('[] :: [Peano]) a) Source #
Instance details Defined in Termonad.Config.Vec Methods (+) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # (-) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # (*) :: Matrix '[] a -> Matrix '[] a -> Matrix '[] a # negate :: Matrix '[] a -> Matrix '[] a # abs :: Matrix '[] a -> Matrix '[] a # signum :: Matrix '[] a -> Matrix '[] a # fromInteger :: Integer -> Matrix '[] a #
Ord (MatrixTF ns a) => Ord (Matrix ns a) Source #
Instance details Defined in Termonad.Config.Vec Methods compare :: Matrix ns a -> Matrix ns a -> Ordering # (<) :: Matrix ns a -> Matrix ns a -> Bool # (<=) :: Matrix ns a -> Matrix ns a -> Bool # (>) :: Matrix ns a -> Matrix ns a -> Bool # (>=) :: Matrix ns a -> Matrix ns a -> Bool # max :: Matrix ns a -> Matrix ns a -> Matrix ns a # min :: Matrix ns a -> Matrix ns a -> Matrix ns a #
Show (MatrixTF ns a) => Show (Matrix ns a) Source #
Instance details Defined in Termonad.Config.Vec Methods showsPrec :: Int -> Matrix ns a -> ShowS # show :: Matrix ns a -> String # showList :: [Matrix ns a] -> ShowS #
SingI ns => MonoFoldable (Matrix ns a) Source #
Instance details Defined in Termonad.Config.Vec Methods ofoldMap :: Monoid m => (Element (Matrix ns a) -> m) -> Matrix ns a -> m Source # ofoldr :: (Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b Source # ofoldl' :: (a0 -> Element (Matrix ns a) -> a0) -> a0 -> Matrix ns a -> a0 Source # otoList :: Matrix ns a -> [Element (Matrix ns a)] Source # oall :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool Source # oany :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool Source # onull :: Matrix ns a -> Bool Source # olength :: Matrix ns a -> Int Source # olength64 :: Matrix ns a -> Int64 Source # ocompareLength :: Integral i => Matrix ns a -> i -> Ordering Source # otraverse_ :: Applicative f => (Element (Matrix ns a) -> f b) -> Matrix ns a -> f () Source # ofor_ :: Applicative f => Matrix ns a -> (Element (Matrix ns a) -> f b) -> f () Source # omapM_ :: Applicative m => (Element (Matrix ns a) -> m ()) -> Matrix ns a -> m () Source # oforM_ :: Applicative m => Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m () Source # ofoldlM :: Monad m => (a0 -> Element (Matrix ns a) -> m a0) -> a0 -> Matrix ns a -> m a0 Source # ofoldMap1Ex :: Semigroup m => (Element (Matrix ns a) -> m) -> Matrix ns a -> m Source # ofoldr1Ex :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Element (Matrix ns a)) -> Matrix ns a -> Element (Matrix ns a) Source # ofoldl1Ex' :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Element (Matrix ns a)) -> Matrix ns a -> Element (Matrix ns a) Source # headEx :: Matrix ns a -> Element (Matrix ns a) Source # lastEx :: Matrix ns a -> Element (Matrix ns a) Source # unsafeHead :: Matrix ns a -> Element (Matrix ns a) Source # unsafeLast :: Matrix ns a -> Element (Matrix ns a) Source # maximumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering) -> Matrix ns a -> Element (Matrix ns a) Source # minimumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering) -> Matrix ns a -> Element (Matrix ns a) Source # oelem :: Element (Matrix ns a) -> Matrix ns a -> Bool Source # onotElem :: Element (Matrix ns a) -> Matrix ns a -> Bool Source #
type Rep (Matrix ns) Source #
Instance details Defined in Termonad.Config.Vec type Rep (Matrix ns) = HList Fin ns
type Element (Matrix ns a) Source #
Instance details Defined in Termonad.Config.Vec type Element (Matrix ns a) = a

type MatrixTFSym2 (ns :: [Peano]) (t :: Type) = MatrixTF ns t :: Type Source #

data MatrixTFSym1 (ns :: [Peano]) (z :: TyFun Type Type) Source #

Constructors

forall (arg :: Type).SameKind (Apply (MatrixTFSym1 ns) arg) (MatrixTFSym2 ns arg) => MatrixTFSym1KindInference

Instances

Instances details

type Apply (MatrixTFSym1 l1 :: TyFun Type Type -> Type) (l2 :: Type) Source #
Instance details Defined in Termonad.Config.Vec type Apply (MatrixTFSym1 l1 :: TyFun Type Type -> Type) (l2 :: Type) = MatrixTF l1 l2

data MatrixTFSym0 (l :: TyFun [Peano] (Type ~> Type)) Source #

Constructors

forall (arg :: [Peano]).SameKind (Apply MatrixTFSym0 arg) (MatrixTFSym1 arg) => MatrixTFSym0KindInference

Instances

Instances details

type Apply MatrixTFSym0 (l :: [Peano]) Source #
Instance details Defined in Termonad.Config.Vec type Apply MatrixTFSym0 (l :: [Peano]) = MatrixTFSym1 l

eqSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Eq a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Bool Source #

ordSingMatrix :: forall (peanos :: [Peano]) (a :: Type). Ord a => Sing peanos -> Matrix peanos a -> Matrix peanos a -> Ordering Source #

compareSingMatrix :: forall (peanos :: [Peano]) (a :: Type) (c :: Type). (a -> a -> c) -> c -> (c -> c -> c) -> Sing peanos -> Matrix peanos a -> Matrix peanos a -> c Source #

fmapSingMatrix :: forall (peanos :: [Peano]) (a :: Type) (b :: Type). Sing peanos -> (a -> b) -> Matrix peanos a -> Matrix peanos b Source #

consMatrix :: Matrix ns a -> Matrix (n ': ns) a -> Matrix ('S n ': ns) a Source #

toListMatrix :: forall (peanos :: [Peano]) (a :: Type). Sing peanos -> Matrix peanos a -> [a] Source #

genMatrix :: forall (ns :: [Peano]) (a :: Type). Sing ns -> (HList Fin ns -> a) -> Matrix ns a Source #

genMatrix_ :: SingI ns => (HList Fin ns -> a) -> Matrix ns a Source #

indexMatrix :: HList Fin ns -> Matrix ns a -> a Source #

imapMatrix :: forall (ns :: [Peano]) a b. Sing ns -> (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b Source #

imapMatrix_ :: SingI ns => (HList Fin ns -> a -> b) -> Matrix ns a -> Matrix ns b Source #

onMatrixTF :: (MatrixTF ns a -> MatrixTF ms b) -> Matrix ns a -> Matrix ms b Source #

onMatrix :: (Matrix ns a -> Matrix ms b) -> MatrixTF ns a -> MatrixTF ms b Source #

updateAtMatrix :: HList Fin ns -> (a -> a) -> Matrix ns a -> Matrix ns a Source #

setAtMatrix :: HList Fin ns -> a -> Matrix ns a -> Matrix ns a Source #