Copyright | (c) Dennis Gosnell 2018 |
---|---|
License | BSD3 |
Stability | experimental |
Portability | POSIX |
Safe Haskell | None |
Language | Haskell2010 |
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
- type ZSym0 = Z
- type SSym1 (t6989586621679500065 :: Peano) = S t6989586621679500065
- data SSym0 :: (~>) Peano Peano where
- 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 a6989586621679500073 arg. SameKind (Apply SubtractPeanoSym0 arg) (SubtractPeanoSym1 arg) => SubtractPeanoSym0 a6989586621679500073
- data SubtractPeanoSym1 (a6989586621679500073 :: Peano) :: (~>) Peano Peano where
- SubtractPeanoSym1KindInference :: forall a6989586621679500073 a6989586621679500074 arg. SameKind (Apply (SubtractPeanoSym1 a6989586621679500073) arg) (SubtractPeanoSym2 a6989586621679500073 arg) => SubtractPeanoSym1 a6989586621679500073 a6989586621679500074
- type SubtractPeanoSym2 (a6989586621679500073 :: Peano) (a6989586621679500074 :: Peano) = SubtractPeano a6989586621679500073 a6989586621679500074
- type family AddPeano (a :: Peano) (a :: Peano) :: Peano where ...
- data AddPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where
- AddPeanoSym0KindInference :: forall a6989586621679500080 arg. SameKind (Apply AddPeanoSym0 arg) (AddPeanoSym1 arg) => AddPeanoSym0 a6989586621679500080
- data AddPeanoSym1 (a6989586621679500080 :: Peano) :: (~>) Peano Peano where
- AddPeanoSym1KindInference :: forall a6989586621679500080 a6989586621679500081 arg. SameKind (Apply (AddPeanoSym1 a6989586621679500080) arg) (AddPeanoSym2 a6989586621679500080 arg) => AddPeanoSym1 a6989586621679500080 a6989586621679500081
- type AddPeanoSym2 (a6989586621679500080 :: Peano) (a6989586621679500081 :: Peano) = AddPeano a6989586621679500080 a6989586621679500081
- type family MultPeano (a :: Peano) (a :: Peano) :: Peano where ...
- data MultPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where
- MultPeanoSym0KindInference :: forall a6989586621679500067 arg. SameKind (Apply MultPeanoSym0 arg) (MultPeanoSym1 arg) => MultPeanoSym0 a6989586621679500067
- data MultPeanoSym1 (a6989586621679500067 :: Peano) :: (~>) Peano Peano where
- MultPeanoSym1KindInference :: forall a6989586621679500067 a6989586621679500068 arg. SameKind (Apply (MultPeanoSym1 a6989586621679500067) arg) (MultPeanoSym2 a6989586621679500067 arg) => MultPeanoSym1 a6989586621679500067 a6989586621679500068
- type MultPeanoSym2 (a6989586621679500067 :: Peano) (a6989586621679500068 :: Peano) = MultPeano a6989586621679500067 a6989586621679500068
- type family N24 :: Peano where ...
- type N24Sym0 = N24
- type family Compare_6989586621679501810 (a :: Peano) (a :: Peano) :: Ordering where ...
- type Compare_6989586621679501810Sym2 (a6989586621679501808 :: Peano) (a6989586621679501809 :: Peano) = Compare_6989586621679501810 a6989586621679501808 a6989586621679501809
- data Compare_6989586621679501810Sym1 (a6989586621679501808 :: Peano) :: (~>) Peano Ordering where
- Compare_6989586621679501810Sym1KindInference :: forall a6989586621679501808 a6989586621679501809 arg. SameKind (Apply (Compare_6989586621679501810Sym1 a6989586621679501808) arg) (Compare_6989586621679501810Sym2 a6989586621679501808 arg) => Compare_6989586621679501810Sym1 a6989586621679501808 a6989586621679501809
- data Compare_6989586621679501810Sym0 :: (~>) Peano ((~>) Peano Ordering) where
- Compare_6989586621679501810Sym0KindInference :: forall a6989586621679501808 arg. SameKind (Apply Compare_6989586621679501810Sym0 arg) (Compare_6989586621679501810Sym1 arg) => Compare_6989586621679501810Sym0 a6989586621679501808
- type family ShowsPrec_6989586621679502503 (a :: Nat) (a :: Peano) (a :: Symbol) :: Symbol where ...
- type ShowsPrec_6989586621679502503Sym3 (a6989586621679502500 :: Nat) (a6989586621679502501 :: Peano) (a6989586621679502502 :: Symbol) = ShowsPrec_6989586621679502503 a6989586621679502500 a6989586621679502501 a6989586621679502502
- data ShowsPrec_6989586621679502503Sym2 (a6989586621679502500 :: Nat) (a6989586621679502501 :: Peano) :: (~>) Symbol Symbol where
- ShowsPrec_6989586621679502503Sym2KindInference :: forall a6989586621679502500 a6989586621679502501 a6989586621679502502 arg. SameKind (Apply (ShowsPrec_6989586621679502503Sym2 a6989586621679502500 a6989586621679502501) arg) (ShowsPrec_6989586621679502503Sym3 a6989586621679502500 a6989586621679502501 arg) => ShowsPrec_6989586621679502503Sym2 a6989586621679502500 a6989586621679502501 a6989586621679502502
- data ShowsPrec_6989586621679502503Sym1 (a6989586621679502500 :: Nat) :: (~>) Peano ((~>) Symbol Symbol) where
- ShowsPrec_6989586621679502503Sym1KindInference :: forall a6989586621679502500 a6989586621679502501 arg. SameKind (Apply (ShowsPrec_6989586621679502503Sym1 a6989586621679502500) arg) (ShowsPrec_6989586621679502503Sym2 a6989586621679502500 arg) => ShowsPrec_6989586621679502503Sym1 a6989586621679502500 a6989586621679502501
- data ShowsPrec_6989586621679502503Sym0 :: (~>) Nat ((~>) Peano ((~>) Symbol Symbol)) where
- ShowsPrec_6989586621679502503Sym0KindInference :: forall a6989586621679502500 arg. SameKind (Apply ShowsPrec_6989586621679502503Sym0 arg) (ShowsPrec_6989586621679502503Sym1 arg) => ShowsPrec_6989586621679502503Sym0 a6989586621679502500
- type family TFHelper_6989586621679503044 (a :: Peano) (a :: Peano) :: Peano where ...
- type TFHelper_6989586621679503044Sym2 (a6989586621679503042 :: Peano) (a6989586621679503043 :: Peano) = TFHelper_6989586621679503044 a6989586621679503042 a6989586621679503043
- data TFHelper_6989586621679503044Sym1 (a6989586621679503042 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679503044Sym1KindInference :: forall a6989586621679503042 a6989586621679503043 arg. SameKind (Apply (TFHelper_6989586621679503044Sym1 a6989586621679503042) arg) (TFHelper_6989586621679503044Sym2 a6989586621679503042 arg) => TFHelper_6989586621679503044Sym1 a6989586621679503042 a6989586621679503043
- data TFHelper_6989586621679503044Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679503044Sym0KindInference :: forall a6989586621679503042 arg. SameKind (Apply TFHelper_6989586621679503044Sym0 arg) (TFHelper_6989586621679503044Sym1 arg) => TFHelper_6989586621679503044Sym0 a6989586621679503042
- type family TFHelper_6989586621679503060 (a :: Peano) (a :: Peano) :: Peano where ...
- type TFHelper_6989586621679503060Sym2 (a6989586621679503058 :: Peano) (a6989586621679503059 :: Peano) = TFHelper_6989586621679503060 a6989586621679503058 a6989586621679503059
- data TFHelper_6989586621679503060Sym1 (a6989586621679503058 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679503060Sym1KindInference :: forall a6989586621679503058 a6989586621679503059 arg. SameKind (Apply (TFHelper_6989586621679503060Sym1 a6989586621679503058) arg) (TFHelper_6989586621679503060Sym2 a6989586621679503058 arg) => TFHelper_6989586621679503060Sym1 a6989586621679503058 a6989586621679503059
- data TFHelper_6989586621679503060Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679503060Sym0KindInference :: forall a6989586621679503058 arg. SameKind (Apply TFHelper_6989586621679503060Sym0 arg) (TFHelper_6989586621679503060Sym1 arg) => TFHelper_6989586621679503060Sym0 a6989586621679503058
- type family TFHelper_6989586621679503076 (a :: Peano) (a :: Peano) :: Peano where ...
- type TFHelper_6989586621679503076Sym2 (a6989586621679503074 :: Peano) (a6989586621679503075 :: Peano) = TFHelper_6989586621679503076 a6989586621679503074 a6989586621679503075
- data TFHelper_6989586621679503076Sym1 (a6989586621679503074 :: Peano) :: (~>) Peano Peano where
- TFHelper_6989586621679503076Sym1KindInference :: forall a6989586621679503074 a6989586621679503075 arg. SameKind (Apply (TFHelper_6989586621679503076Sym1 a6989586621679503074) arg) (TFHelper_6989586621679503076Sym2 a6989586621679503074 arg) => TFHelper_6989586621679503076Sym1 a6989586621679503074 a6989586621679503075
- data TFHelper_6989586621679503076Sym0 :: (~>) Peano ((~>) Peano Peano) where
- TFHelper_6989586621679503076Sym0KindInference :: forall a6989586621679503074 arg. SameKind (Apply TFHelper_6989586621679503076Sym0 arg) (TFHelper_6989586621679503076Sym1 arg) => TFHelper_6989586621679503076Sym0 a6989586621679503074
- type family Abs_6989586621679503091 (a :: Peano) :: Peano where ...
- type Abs_6989586621679503091Sym1 (a6989586621679503090 :: Peano) = Abs_6989586621679503091 a6989586621679503090
- data Abs_6989586621679503091Sym0 :: (~>) Peano Peano where
- Abs_6989586621679503091Sym0KindInference :: forall a6989586621679503090 arg. SameKind (Apply Abs_6989586621679503091Sym0 arg) (Abs_6989586621679503091Sym1 arg) => Abs_6989586621679503091Sym0 a6989586621679503090
- type family Signum_6989586621679503100 (a :: Peano) :: Peano where ...
- type Signum_6989586621679503100Sym1 (a6989586621679503099 :: Peano) = Signum_6989586621679503100 a6989586621679503099
- data Signum_6989586621679503100Sym0 :: (~>) Peano Peano where
- Signum_6989586621679503100Sym0KindInference :: forall a6989586621679503099 arg. SameKind (Apply Signum_6989586621679503100Sym0 arg) (Signum_6989586621679503100Sym1 arg) => Signum_6989586621679503100Sym0 a6989586621679503099
- type family Let6989586621679503111Scrutinee_6989586621679488366 n where ...
- type Let6989586621679503111Scrutinee_6989586621679488366Sym1 n6989586621679503110 = Let6989586621679503111Scrutinee_6989586621679488366 n6989586621679503110
- data Let6989586621679503111Scrutinee_6989586621679488366Sym0 n6989586621679503110 where
- Let6989586621679503111Scrutinee_6989586621679488366Sym0KindInference :: forall n6989586621679503110 arg. SameKind (Apply Let6989586621679503111Scrutinee_6989586621679488366Sym0 arg) (Let6989586621679503111Scrutinee_6989586621679488366Sym1 arg) => Let6989586621679503111Scrutinee_6989586621679488366Sym0 n6989586621679503110
- type family Let6989586621679503115Scrutinee_6989586621679488368 n where ...
- type Let6989586621679503115Scrutinee_6989586621679488368Sym1 n6989586621679503110 = Let6989586621679503115Scrutinee_6989586621679488368 n6989586621679503110
- data Let6989586621679503115Scrutinee_6989586621679488368Sym0 n6989586621679503110 where
- Let6989586621679503115Scrutinee_6989586621679488368Sym0KindInference :: forall n6989586621679503110 arg. SameKind (Apply Let6989586621679503115Scrutinee_6989586621679488368Sym0 arg) (Let6989586621679503115Scrutinee_6989586621679488368Sym1 arg) => Let6989586621679503115Scrutinee_6989586621679488368Sym0 n6989586621679503110
- type family Case_6989586621679503117 n t where ...
- type family Case_6989586621679503113 n t where ...
- type family FromInteger_6989586621679503106 (a :: Nat) :: Peano where ...
- type FromInteger_6989586621679503106Sym1 (a6989586621679503105 :: Nat) = FromInteger_6989586621679503106 a6989586621679503105
- data FromInteger_6989586621679503106Sym0 :: (~>) Nat Peano where
- FromInteger_6989586621679503106Sym0KindInference :: forall a6989586621679503105 arg. SameKind (Apply FromInteger_6989586621679503106Sym0 arg) (FromInteger_6989586621679503106Sym1 arg) => FromInteger_6989586621679503106Sym0 a6989586621679503105
- type family Equals_6989586621679503122 (a :: Peano) (b :: Peano) :: Bool where ...
- data SPeano :: Peano -> Type where
- 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
- 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
- data IFin :: Peano -> Peano -> Type where
- 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
- data HList :: (k -> Type) -> [k] -> Type where
- pattern ConsHList :: (f a :: Type) -> HList f as -> HList f (a ': as)
- data Vec (n :: Peano) :: Type -> Type where
- 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 {}
- 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
Instances
data SSym0 :: (~>) Peano Peano where Source #
SSym0KindInference :: forall t6989586621679500065 arg. SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0 t6989586621679500065 |
Instances
SuppressUnusedWarnings SSym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI SSym0 Source # | |
Defined in Termonad.Config.Vec | |
type Apply SSym0 (t6989586621679500065 :: Peano) Source # | |
Defined in Termonad.Config.Vec |
type family SubtractPeano (a :: Peano) (a :: Peano) :: Peano where ... Source #
SubtractPeano Z _ = ZSym0 | |
SubtractPeano a Z = a | |
SubtractPeano (S a) (S b) = Apply (Apply SubtractPeanoSym0 a) b |
data SubtractPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #
SubtractPeanoSym0KindInference :: forall a6989586621679500073 arg. SameKind (Apply SubtractPeanoSym0 arg) (SubtractPeanoSym1 arg) => SubtractPeanoSym0 a6989586621679500073 |
Instances
SuppressUnusedWarnings SubtractPeanoSym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI SubtractPeanoSym0 Source # | |
Defined in Termonad.Config.Vec | |
type Apply SubtractPeanoSym0 (a6989586621679500073 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply SubtractPeanoSym0 (a6989586621679500073 :: Peano) = SubtractPeanoSym1 a6989586621679500073 |
data SubtractPeanoSym1 (a6989586621679500073 :: Peano) :: (~>) Peano Peano where Source #
SubtractPeanoSym1KindInference :: forall a6989586621679500073 a6989586621679500074 arg. SameKind (Apply (SubtractPeanoSym1 a6989586621679500073) arg) (SubtractPeanoSym2 a6989586621679500073 arg) => SubtractPeanoSym1 a6989586621679500073 a6989586621679500074 |
Instances
SuppressUnusedWarnings (SubtractPeanoSym1 a6989586621679500073 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI d => SingI (SubtractPeanoSym1 d :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec sing :: Sing (SubtractPeanoSym1 d) # | |
type Apply (SubtractPeanoSym1 a6989586621679500073 :: TyFun Peano Peano -> Type) (a6989586621679500074 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (SubtractPeanoSym1 a6989586621679500073 :: TyFun Peano Peano -> Type) (a6989586621679500074 :: Peano) = SubtractPeano a6989586621679500073 a6989586621679500074 |
type SubtractPeanoSym2 (a6989586621679500073 :: Peano) (a6989586621679500074 :: Peano) = SubtractPeano a6989586621679500073 a6989586621679500074 Source #
data AddPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #
AddPeanoSym0KindInference :: forall a6989586621679500080 arg. SameKind (Apply AddPeanoSym0 arg) (AddPeanoSym1 arg) => AddPeanoSym0 a6989586621679500080 |
Instances
SuppressUnusedWarnings AddPeanoSym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI AddPeanoSym0 Source # | |
Defined in Termonad.Config.Vec sing :: Sing AddPeanoSym0 # | |
type Apply AddPeanoSym0 (a6989586621679500080 :: Peano) Source # | |
Defined in Termonad.Config.Vec |
data AddPeanoSym1 (a6989586621679500080 :: Peano) :: (~>) Peano Peano where Source #
AddPeanoSym1KindInference :: forall a6989586621679500080 a6989586621679500081 arg. SameKind (Apply (AddPeanoSym1 a6989586621679500080) arg) (AddPeanoSym2 a6989586621679500080 arg) => AddPeanoSym1 a6989586621679500080 a6989586621679500081 |
Instances
SuppressUnusedWarnings (AddPeanoSym1 a6989586621679500080 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI d => SingI (AddPeanoSym1 d :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec sing :: Sing (AddPeanoSym1 d) # | |
type Apply (AddPeanoSym1 a6989586621679500080 :: TyFun Peano Peano -> Type) (a6989586621679500081 :: Peano) Source # | |
Defined in Termonad.Config.Vec |
type AddPeanoSym2 (a6989586621679500080 :: Peano) (a6989586621679500081 :: Peano) = AddPeano a6989586621679500080 a6989586621679500081 Source #
data MultPeanoSym0 :: (~>) Peano ((~>) Peano Peano) where Source #
MultPeanoSym0KindInference :: forall a6989586621679500067 arg. SameKind (Apply MultPeanoSym0 arg) (MultPeanoSym1 arg) => MultPeanoSym0 a6989586621679500067 |
Instances
SuppressUnusedWarnings MultPeanoSym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI MultPeanoSym0 Source # | |
Defined in Termonad.Config.Vec sing :: Sing MultPeanoSym0 # | |
type Apply MultPeanoSym0 (a6989586621679500067 :: Peano) Source # | |
Defined in Termonad.Config.Vec |
data MultPeanoSym1 (a6989586621679500067 :: Peano) :: (~>) Peano Peano where Source #
MultPeanoSym1KindInference :: forall a6989586621679500067 a6989586621679500068 arg. SameKind (Apply (MultPeanoSym1 a6989586621679500067) arg) (MultPeanoSym2 a6989586621679500067 arg) => MultPeanoSym1 a6989586621679500067 a6989586621679500068 |
Instances
SuppressUnusedWarnings (MultPeanoSym1 a6989586621679500067 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
SingI d => SingI (MultPeanoSym1 d :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec sing :: Sing (MultPeanoSym1 d) # | |
type Apply (MultPeanoSym1 a6989586621679500067 :: TyFun Peano Peano -> Type) (a6989586621679500068 :: Peano) Source # | |
Defined in Termonad.Config.Vec |
type MultPeanoSym2 (a6989586621679500067 :: Peano) (a6989586621679500068 :: Peano) = MultPeano a6989586621679500067 a6989586621679500068 Source #
type family Compare_6989586621679501810 (a :: Peano) (a :: Peano) :: Ordering where ... Source #
Compare_6989586621679501810 Z Z = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] | |
Compare_6989586621679501810 (S a_6989586621679500055) (S b_6989586621679500057) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_6989586621679500055) b_6989586621679500057)) '[]) | |
Compare_6989586621679501810 Z (S _) = LTSym0 | |
Compare_6989586621679501810 (S _) Z = GTSym0 |
type Compare_6989586621679501810Sym2 (a6989586621679501808 :: Peano) (a6989586621679501809 :: Peano) = Compare_6989586621679501810 a6989586621679501808 a6989586621679501809 Source #
data Compare_6989586621679501810Sym1 (a6989586621679501808 :: Peano) :: (~>) Peano Ordering where Source #
Compare_6989586621679501810Sym1KindInference :: forall a6989586621679501808 a6989586621679501809 arg. SameKind (Apply (Compare_6989586621679501810Sym1 a6989586621679501808) arg) (Compare_6989586621679501810Sym2 a6989586621679501808 arg) => Compare_6989586621679501810Sym1 a6989586621679501808 a6989586621679501809 |
Instances
SuppressUnusedWarnings (Compare_6989586621679501810Sym1 a6989586621679501808 :: TyFun Peano Ordering -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (Compare_6989586621679501810Sym1 a6989586621679501808 :: TyFun Peano Ordering -> Type) (a6989586621679501809 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (Compare_6989586621679501810Sym1 a6989586621679501808 :: TyFun Peano Ordering -> Type) (a6989586621679501809 :: Peano) = Compare_6989586621679501810 a6989586621679501808 a6989586621679501809 |
data Compare_6989586621679501810Sym0 :: (~>) Peano ((~>) Peano Ordering) where Source #
Compare_6989586621679501810Sym0KindInference :: forall a6989586621679501808 arg. SameKind (Apply Compare_6989586621679501810Sym0 arg) (Compare_6989586621679501810Sym1 arg) => Compare_6989586621679501810Sym0 a6989586621679501808 |
Instances
SuppressUnusedWarnings Compare_6989586621679501810Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply Compare_6989586621679501810Sym0 (a6989586621679501808 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply Compare_6989586621679501810Sym0 (a6989586621679501808 :: Peano) = Compare_6989586621679501810Sym1 a6989586621679501808 |
type family ShowsPrec_6989586621679502503 (a :: Nat) (a :: Peano) (a :: Symbol) :: Symbol where ... Source #
ShowsPrec_6989586621679502503 _ Z a_6989586621679502511 = Apply (Apply ShowStringSym0 (FromString "Z")) a_6989586621679502511 | |
ShowsPrec_6989586621679502503 p_6989586621679500059 (S arg_6989586621679500061) a_6989586621679502513 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_6989586621679500059) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 (FromString "S "))) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_6989586621679500061))) a_6989586621679502513 |
type ShowsPrec_6989586621679502503Sym3 (a6989586621679502500 :: Nat) (a6989586621679502501 :: Peano) (a6989586621679502502 :: Symbol) = ShowsPrec_6989586621679502503 a6989586621679502500 a6989586621679502501 a6989586621679502502 Source #
data ShowsPrec_6989586621679502503Sym2 (a6989586621679502500 :: Nat) (a6989586621679502501 :: Peano) :: (~>) Symbol Symbol where Source #
ShowsPrec_6989586621679502503Sym2KindInference :: forall a6989586621679502500 a6989586621679502501 a6989586621679502502 arg. SameKind (Apply (ShowsPrec_6989586621679502503Sym2 a6989586621679502500 a6989586621679502501) arg) (ShowsPrec_6989586621679502503Sym3 a6989586621679502500 a6989586621679502501 arg) => ShowsPrec_6989586621679502503Sym2 a6989586621679502500 a6989586621679502501 a6989586621679502502 |
Instances
SuppressUnusedWarnings (ShowsPrec_6989586621679502503Sym2 a6989586621679502501 a6989586621679502500 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (ShowsPrec_6989586621679502503Sym2 a6989586621679502501 a6989586621679502500 :: TyFun Symbol Symbol -> Type) (a6989586621679502502 :: Symbol) Source # | |
Defined in Termonad.Config.Vec type Apply (ShowsPrec_6989586621679502503Sym2 a6989586621679502501 a6989586621679502500 :: TyFun Symbol Symbol -> Type) (a6989586621679502502 :: Symbol) = ShowsPrec_6989586621679502503 a6989586621679502501 a6989586621679502500 a6989586621679502502 |
data ShowsPrec_6989586621679502503Sym1 (a6989586621679502500 :: Nat) :: (~>) Peano ((~>) Symbol Symbol) where Source #
ShowsPrec_6989586621679502503Sym1KindInference :: forall a6989586621679502500 a6989586621679502501 arg. SameKind (Apply (ShowsPrec_6989586621679502503Sym1 a6989586621679502500) arg) (ShowsPrec_6989586621679502503Sym2 a6989586621679502500 arg) => ShowsPrec_6989586621679502503Sym1 a6989586621679502500 a6989586621679502501 |
Instances
SuppressUnusedWarnings (ShowsPrec_6989586621679502503Sym1 a6989586621679502500 :: TyFun Peano (Symbol ~> Symbol) -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (ShowsPrec_6989586621679502503Sym1 a6989586621679502500 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679502501 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (ShowsPrec_6989586621679502503Sym1 a6989586621679502500 :: TyFun Peano (Symbol ~> Symbol) -> Type) (a6989586621679502501 :: Peano) = ShowsPrec_6989586621679502503Sym2 a6989586621679502500 a6989586621679502501 |
data ShowsPrec_6989586621679502503Sym0 :: (~>) Nat ((~>) Peano ((~>) Symbol Symbol)) where Source #
ShowsPrec_6989586621679502503Sym0KindInference :: forall a6989586621679502500 arg. SameKind (Apply ShowsPrec_6989586621679502503Sym0 arg) (ShowsPrec_6989586621679502503Sym1 arg) => ShowsPrec_6989586621679502503Sym0 a6989586621679502500 |
Instances
SuppressUnusedWarnings ShowsPrec_6989586621679502503Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply ShowsPrec_6989586621679502503Sym0 (a6989586621679502500 :: Nat) Source # | |
Defined in Termonad.Config.Vec type Apply ShowsPrec_6989586621679502503Sym0 (a6989586621679502500 :: Nat) = ShowsPrec_6989586621679502503Sym1 a6989586621679502500 |
type family TFHelper_6989586621679503044 (a :: Peano) (a :: Peano) :: Peano where ... Source #
TFHelper_6989586621679503044 a_6989586621679503046 a_6989586621679503048 = Apply (Apply AddPeanoSym0 a_6989586621679503046) a_6989586621679503048 |
type TFHelper_6989586621679503044Sym2 (a6989586621679503042 :: Peano) (a6989586621679503043 :: Peano) = TFHelper_6989586621679503044 a6989586621679503042 a6989586621679503043 Source #
data TFHelper_6989586621679503044Sym1 (a6989586621679503042 :: Peano) :: (~>) Peano Peano where Source #
TFHelper_6989586621679503044Sym1KindInference :: forall a6989586621679503042 a6989586621679503043 arg. SameKind (Apply (TFHelper_6989586621679503044Sym1 a6989586621679503042) arg) (TFHelper_6989586621679503044Sym2 a6989586621679503042 arg) => TFHelper_6989586621679503044Sym1 a6989586621679503042 a6989586621679503043 |
Instances
SuppressUnusedWarnings (TFHelper_6989586621679503044Sym1 a6989586621679503042 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (TFHelper_6989586621679503044Sym1 a6989586621679503042 :: TyFun Peano Peano -> Type) (a6989586621679503043 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679503044Sym1 a6989586621679503042 :: TyFun Peano Peano -> Type) (a6989586621679503043 :: Peano) = TFHelper_6989586621679503044 a6989586621679503042 a6989586621679503043 |
data TFHelper_6989586621679503044Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #
TFHelper_6989586621679503044Sym0KindInference :: forall a6989586621679503042 arg. SameKind (Apply TFHelper_6989586621679503044Sym0 arg) (TFHelper_6989586621679503044Sym1 arg) => TFHelper_6989586621679503044Sym0 a6989586621679503042 |
Instances
SuppressUnusedWarnings TFHelper_6989586621679503044Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply TFHelper_6989586621679503044Sym0 (a6989586621679503042 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679503044Sym0 (a6989586621679503042 :: Peano) = TFHelper_6989586621679503044Sym1 a6989586621679503042 |
type family TFHelper_6989586621679503060 (a :: Peano) (a :: Peano) :: Peano where ... Source #
TFHelper_6989586621679503060 a_6989586621679503062 a_6989586621679503064 = Apply (Apply SubtractPeanoSym0 a_6989586621679503062) a_6989586621679503064 |
type TFHelper_6989586621679503060Sym2 (a6989586621679503058 :: Peano) (a6989586621679503059 :: Peano) = TFHelper_6989586621679503060 a6989586621679503058 a6989586621679503059 Source #
data TFHelper_6989586621679503060Sym1 (a6989586621679503058 :: Peano) :: (~>) Peano Peano where Source #
TFHelper_6989586621679503060Sym1KindInference :: forall a6989586621679503058 a6989586621679503059 arg. SameKind (Apply (TFHelper_6989586621679503060Sym1 a6989586621679503058) arg) (TFHelper_6989586621679503060Sym2 a6989586621679503058 arg) => TFHelper_6989586621679503060Sym1 a6989586621679503058 a6989586621679503059 |
Instances
SuppressUnusedWarnings (TFHelper_6989586621679503060Sym1 a6989586621679503058 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (TFHelper_6989586621679503060Sym1 a6989586621679503058 :: TyFun Peano Peano -> Type) (a6989586621679503059 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679503060Sym1 a6989586621679503058 :: TyFun Peano Peano -> Type) (a6989586621679503059 :: Peano) = TFHelper_6989586621679503060 a6989586621679503058 a6989586621679503059 |
data TFHelper_6989586621679503060Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #
TFHelper_6989586621679503060Sym0KindInference :: forall a6989586621679503058 arg. SameKind (Apply TFHelper_6989586621679503060Sym0 arg) (TFHelper_6989586621679503060Sym1 arg) => TFHelper_6989586621679503060Sym0 a6989586621679503058 |
Instances
SuppressUnusedWarnings TFHelper_6989586621679503060Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply TFHelper_6989586621679503060Sym0 (a6989586621679503058 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679503060Sym0 (a6989586621679503058 :: Peano) = TFHelper_6989586621679503060Sym1 a6989586621679503058 |
type family TFHelper_6989586621679503076 (a :: Peano) (a :: Peano) :: Peano where ... Source #
TFHelper_6989586621679503076 a_6989586621679503078 a_6989586621679503080 = Apply (Apply MultPeanoSym0 a_6989586621679503078) a_6989586621679503080 |
type TFHelper_6989586621679503076Sym2 (a6989586621679503074 :: Peano) (a6989586621679503075 :: Peano) = TFHelper_6989586621679503076 a6989586621679503074 a6989586621679503075 Source #
data TFHelper_6989586621679503076Sym1 (a6989586621679503074 :: Peano) :: (~>) Peano Peano where Source #
TFHelper_6989586621679503076Sym1KindInference :: forall a6989586621679503074 a6989586621679503075 arg. SameKind (Apply (TFHelper_6989586621679503076Sym1 a6989586621679503074) arg) (TFHelper_6989586621679503076Sym2 a6989586621679503074 arg) => TFHelper_6989586621679503076Sym1 a6989586621679503074 a6989586621679503075 |
Instances
SuppressUnusedWarnings (TFHelper_6989586621679503076Sym1 a6989586621679503074 :: TyFun Peano Peano -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (TFHelper_6989586621679503076Sym1 a6989586621679503074 :: TyFun Peano Peano -> Type) (a6989586621679503075 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply (TFHelper_6989586621679503076Sym1 a6989586621679503074 :: TyFun Peano Peano -> Type) (a6989586621679503075 :: Peano) = TFHelper_6989586621679503076 a6989586621679503074 a6989586621679503075 |
data TFHelper_6989586621679503076Sym0 :: (~>) Peano ((~>) Peano Peano) where Source #
TFHelper_6989586621679503076Sym0KindInference :: forall a6989586621679503074 arg. SameKind (Apply TFHelper_6989586621679503076Sym0 arg) (TFHelper_6989586621679503076Sym1 arg) => TFHelper_6989586621679503076Sym0 a6989586621679503074 |
Instances
SuppressUnusedWarnings TFHelper_6989586621679503076Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply TFHelper_6989586621679503076Sym0 (a6989586621679503074 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply TFHelper_6989586621679503076Sym0 (a6989586621679503074 :: Peano) = TFHelper_6989586621679503076Sym1 a6989586621679503074 |
type family Abs_6989586621679503091 (a :: Peano) :: Peano where ... Source #
Abs_6989586621679503091 a_6989586621679503093 = Apply IdSym0 a_6989586621679503093 |
type Abs_6989586621679503091Sym1 (a6989586621679503090 :: Peano) = Abs_6989586621679503091 a6989586621679503090 Source #
data Abs_6989586621679503091Sym0 :: (~>) Peano Peano where Source #
Abs_6989586621679503091Sym0KindInference :: forall a6989586621679503090 arg. SameKind (Apply Abs_6989586621679503091Sym0 arg) (Abs_6989586621679503091Sym1 arg) => Abs_6989586621679503091Sym0 a6989586621679503090 |
Instances
SuppressUnusedWarnings Abs_6989586621679503091Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply Abs_6989586621679503091Sym0 (a6989586621679503090 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply Abs_6989586621679503091Sym0 (a6989586621679503090 :: Peano) = Abs_6989586621679503091 a6989586621679503090 |
type family Signum_6989586621679503100 (a :: Peano) :: Peano where ... Source #
type Signum_6989586621679503100Sym1 (a6989586621679503099 :: Peano) = Signum_6989586621679503100 a6989586621679503099 Source #
data Signum_6989586621679503100Sym0 :: (~>) Peano Peano where Source #
Signum_6989586621679503100Sym0KindInference :: forall a6989586621679503099 arg. SameKind (Apply Signum_6989586621679503100Sym0 arg) (Signum_6989586621679503100Sym1 arg) => Signum_6989586621679503100Sym0 a6989586621679503099 |
Instances
SuppressUnusedWarnings Signum_6989586621679503100Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply Signum_6989586621679503100Sym0 (a6989586621679503099 :: Peano) Source # | |
Defined in Termonad.Config.Vec type Apply Signum_6989586621679503100Sym0 (a6989586621679503099 :: Peano) = Signum_6989586621679503100 a6989586621679503099 |
type family Let6989586621679503111Scrutinee_6989586621679488366 n where ... Source #
type Let6989586621679503111Scrutinee_6989586621679488366Sym1 n6989586621679503110 = Let6989586621679503111Scrutinee_6989586621679488366 n6989586621679503110 Source #
data Let6989586621679503111Scrutinee_6989586621679488366Sym0 n6989586621679503110 where Source #
Let6989586621679503111Scrutinee_6989586621679488366Sym0KindInference :: forall n6989586621679503110 arg. SameKind (Apply Let6989586621679503111Scrutinee_6989586621679488366Sym0 arg) (Let6989586621679503111Scrutinee_6989586621679488366Sym1 arg) => Let6989586621679503111Scrutinee_6989586621679488366Sym0 n6989586621679503110 |
Instances
SuppressUnusedWarnings (Let6989586621679503111Scrutinee_6989586621679488366Sym0 :: TyFun k1 Bool -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (Let6989586621679503111Scrutinee_6989586621679488366Sym0 :: TyFun k1 Bool -> Type) (n6989586621679503110 :: k1) Source # | |
Defined in Termonad.Config.Vec type Apply (Let6989586621679503111Scrutinee_6989586621679488366Sym0 :: TyFun k1 Bool -> Type) (n6989586621679503110 :: k1) = Let6989586621679503111Scrutinee_6989586621679488366 n6989586621679503110 |
type family Let6989586621679503115Scrutinee_6989586621679488368 n where ... Source #
type Let6989586621679503115Scrutinee_6989586621679488368Sym1 n6989586621679503110 = Let6989586621679503115Scrutinee_6989586621679488368 n6989586621679503110 Source #
data Let6989586621679503115Scrutinee_6989586621679488368Sym0 n6989586621679503110 where Source #
Let6989586621679503115Scrutinee_6989586621679488368Sym0KindInference :: forall n6989586621679503110 arg. SameKind (Apply Let6989586621679503115Scrutinee_6989586621679488368Sym0 arg) (Let6989586621679503115Scrutinee_6989586621679488368Sym1 arg) => Let6989586621679503115Scrutinee_6989586621679488368Sym0 n6989586621679503110 |
Instances
SuppressUnusedWarnings (Let6989586621679503115Scrutinee_6989586621679488368Sym0 :: TyFun k1 Bool -> Type) Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply (Let6989586621679503115Scrutinee_6989586621679488368Sym0 :: TyFun k1 Bool -> Type) (n6989586621679503110 :: k1) Source # | |
Defined in Termonad.Config.Vec type Apply (Let6989586621679503115Scrutinee_6989586621679488368Sym0 :: TyFun k1 Bool -> Type) (n6989586621679503110 :: k1) = Let6989586621679503115Scrutinee_6989586621679488368 n6989586621679503110 |
type family Case_6989586621679503117 n t where ... Source #
Case_6989586621679503117 n 'True = ZSym0 | |
Case_6989586621679503117 n 'False = Apply SSym0 (Apply FromIntegerSym0 (Apply (Apply (-@#@$) n) (FromInteger 1))) |
type family Case_6989586621679503113 n t where ... Source #
Case_6989586621679503113 n 'True = Apply ErrorSym0 (FromString "Num Peano fromInteger: n is negative") | |
Case_6989586621679503113 n 'False = Case_6989586621679503117 n (Let6989586621679503115Scrutinee_6989586621679488368Sym1 n) |
type family FromInteger_6989586621679503106 (a :: Nat) :: Peano where ... Source #
type FromInteger_6989586621679503106Sym1 (a6989586621679503105 :: Nat) = FromInteger_6989586621679503106 a6989586621679503105 Source #
data FromInteger_6989586621679503106Sym0 :: (~>) Nat Peano where Source #
FromInteger_6989586621679503106Sym0KindInference :: forall a6989586621679503105 arg. SameKind (Apply FromInteger_6989586621679503106Sym0 arg) (FromInteger_6989586621679503106Sym1 arg) => FromInteger_6989586621679503106Sym0 a6989586621679503105 |
Instances
SuppressUnusedWarnings FromInteger_6989586621679503106Sym0 Source # | |
Defined in Termonad.Config.Vec suppressUnusedWarnings :: () # | |
type Apply FromInteger_6989586621679503106Sym0 (a6989586621679503105 :: Nat) Source # | |
Defined in Termonad.Config.Vec type Apply FromInteger_6989586621679503106Sym0 (a6989586621679503105 :: Nat) = FromInteger_6989586621679503106 a6989586621679503105 |
type family Equals_6989586621679503122 (a :: Peano) (b :: Peano) :: Bool where ... Source #
Equals_6989586621679503122 Z Z = TrueSym0 | |
Equals_6989586621679503122 (S a) (S b) = (==) a b | |
Equals_6989586621679503122 (_ :: Peano) (_ :: Peano) = FalseSym0 |
data SPeano :: Peano -> Type where Source #
Instances
SDecide Peano => TestCoercion SPeano Source # | |
Defined in Termonad.Config.Vec | |
SDecide Peano => TestEquality SPeano Source # | |
Defined in Termonad.Config.Vec | |
ShowSing Peano => Show (SPeano z) Source # | |
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 #
ltSuccProof :: forall (n :: Peano) (m :: Peano) proxy. ('S n < 'S m) ~ 'True => proxy n -> proxy m -> (n < m) :~: 'True Source #
data Fin :: Peano -> Type where Source #
Instances
Eq (Fin n) Source # | |
Ord (Fin n) Source # | |
Show (Fin n) Source # | |
SingKind (Fin n) Source # | |
SingI ('FZ :: Fin ('S n)) Source # | |
Defined in Termonad.Config.Vec | |
SingI n2 => SingI ('FS n2 :: Fin ('S n1)) Source # | |
Defined in Termonad.Config.Vec | |
type Sing Source # | |
Defined in Termonad.Config.Vec | |
type Demote (Fin n) Source # | |
Defined in Termonad.Config.Vec |
data IFin :: Peano -> Peano -> Type where Source #
IFZ :: forall (n :: Peano). IFin ('S n) 'Z | |
IFS :: forall (n :: Peano) (m :: Peano). !(IFin n m) -> IFin ('S n) ('S m) |
Instances
Eq (IFin x y) Source # | |
Ord (IFin x y) Source # | |
Defined in Termonad.Config.Vec | |
Show (IFin x y) Source # | |
SingKind (IFin n m) Source # | |
SingI ('IFZ :: IFin ('S n) 'Z) Source # | |
Defined in Termonad.Config.Vec | |
SingI n2 => SingI ('IFS n2 :: IFin ('S n1) ('S m)) Source # | |
Defined in Termonad.Config.Vec | |
type Sing Source # | |
Defined in Termonad.Config.Vec | |
type Demote (IFin n m) Source # | |
Defined in Termonad.Config.Vec |
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))
pattern ConsHList :: (f a :: Type) -> HList f as -> HList f (a ': as) Source #
Data constructor for :<
.
data Vec (n :: Peano) :: Type -> Type where Source #
Instances
SingI n => Monad (Vec n) Source # | |
Functor (Vec n) Source # | |
SingI n => Applicative (Vec n) Source # | |
Foldable (Vec n) Source # | |
Defined in Termonad.Config.Vec 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 # elem :: Eq a => a -> Vec n a -> Bool # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # | |
SingI n => Distributive (Vec n) Source # | |
SingI n => Representable (Vec n) Source # | |
Eq a => Eq (Vec n a) Source # | |
Ord a => Ord (Vec n a) Source # | |
Show a => Show (Vec n a) Source # | |
SingI n => MonoPointed (Vec n a) Source # | |
MonoFoldable (Vec n a) Source # | |
Defined in Termonad.Config.Vec ofoldMap :: Monoid m => (Element (Vec n a) -> m) -> Vec n a -> m # ofoldr :: (Element (Vec n a) -> b -> b) -> b -> Vec n a -> b # ofoldl' :: (a0 -> Element (Vec n a) -> a0) -> a0 -> Vec n a -> a0 # otoList :: Vec n a -> [Element (Vec n a)] # oall :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool # oany :: (Element (Vec n a) -> Bool) -> Vec n a -> Bool # olength64 :: Vec n a -> Int64 # ocompareLength :: Integral i => Vec n a -> i -> Ordering # otraverse_ :: Applicative f => (Element (Vec n a) -> f b) -> Vec n a -> f () # ofor_ :: Applicative f => Vec n a -> (Element (Vec n a) -> f b) -> f () # omapM_ :: Applicative m => (Element (Vec n a) -> m ()) -> Vec n a -> m () # oforM_ :: Applicative m => Vec n a -> (Element (Vec n a) -> m ()) -> m () # ofoldlM :: Monad m => (a0 -> Element (Vec n a) -> m a0) -> a0 -> Vec n a -> m a0 # ofoldMap1Ex :: Semigroup m => (Element (Vec n a) -> m) -> Vec n a -> m # ofoldr1Ex :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a)) -> Vec n a -> Element (Vec n a) # ofoldl1Ex' :: (Element (Vec n a) -> Element (Vec n a) -> Element (Vec n a)) -> Vec n a -> Element (Vec n a) # headEx :: Vec n a -> Element (Vec n a) # lastEx :: Vec n a -> Element (Vec n a) # unsafeHead :: Vec n a -> Element (Vec n a) # unsafeLast :: Vec n a -> Element (Vec n a) # maximumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering) -> Vec n a -> Element (Vec n a) # minimumByEx :: (Element (Vec n a) -> Element (Vec n a) -> Ordering) -> Vec n a -> Element (Vec n a) # | |
MonoFunctor (Vec n a) Source # | |
type Rep (Vec n) Source # | |
Defined in Termonad.Config.Vec | |
type Element (Vec n a) Source # | |
Defined in Termonad.Config.Vec |
singletonVec :: a -> Vec N1 a Source #
replaceVec :: Sing n -> a -> Vec n a Source #
replaceVec_ :: SingI n => a -> Vec n a Source #
unsafeFromListVec :: Sing n -> [a] -> Vec n a Source #
unsafeFromListVec_ :: SingI n => [a] -> Vec n a Source #
Instances
SingI ns => Monad (Matrix ns) Source # | |
SingI ns => Functor (Matrix ns) Source # | |
SingI ns => Applicative (Matrix ns) Source # | |
SingI ns => Foldable (Matrix ns) Source # | |
Defined in Termonad.Config.Vec 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] # 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 # | |
SingI ns => Distributive (Matrix ns) Source # | |
SingI ns => Representable (Matrix ns) Source # | |
Eq (MatrixTF ns a) => Eq (Matrix ns a) Source # | |
Num a => Num (Matrix ('[] :: [Peano]) a) Source # | |
Defined in Termonad.Config.Vec (+) :: 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 # | |
Defined in Termonad.Config.Vec | |
Show (MatrixTF ns a) => Show (Matrix ns a) Source # | |
SingI ns => MonoFoldable (Matrix ns a) Source # | |
Defined in Termonad.Config.Vec ofoldMap :: Monoid m => (Element (Matrix ns a) -> m) -> Matrix ns a -> m # ofoldr :: (Element (Matrix ns a) -> b -> b) -> b -> Matrix ns a -> b # ofoldl' :: (a0 -> Element (Matrix ns a) -> a0) -> a0 -> Matrix ns a -> a0 # otoList :: Matrix ns a -> [Element (Matrix ns a)] # oall :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool # oany :: (Element (Matrix ns a) -> Bool) -> Matrix ns a -> Bool # onull :: Matrix ns a -> Bool # olength :: Matrix ns a -> Int # olength64 :: Matrix ns a -> Int64 # ocompareLength :: Integral i => Matrix ns a -> i -> Ordering # otraverse_ :: Applicative f => (Element (Matrix ns a) -> f b) -> Matrix ns a -> f () # ofor_ :: Applicative f => Matrix ns a -> (Element (Matrix ns a) -> f b) -> f () # omapM_ :: Applicative m => (Element (Matrix ns a) -> m ()) -> Matrix ns a -> m () # oforM_ :: Applicative m => Matrix ns a -> (Element (Matrix ns a) -> m ()) -> m () # ofoldlM :: Monad m => (a0 -> Element (Matrix ns a) -> m a0) -> a0 -> Matrix ns a -> m a0 # ofoldMap1Ex :: Semigroup m => (Element (Matrix ns a) -> m) -> Matrix ns a -> m # ofoldr1Ex :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Element (Matrix ns a)) -> Matrix ns a -> Element (Matrix ns a) # ofoldl1Ex' :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Element (Matrix ns a)) -> Matrix ns a -> Element (Matrix ns a) # headEx :: Matrix ns a -> Element (Matrix ns a) # lastEx :: Matrix ns a -> Element (Matrix ns a) # unsafeHead :: Matrix ns a -> Element (Matrix ns a) # unsafeLast :: Matrix ns a -> Element (Matrix ns a) # maximumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering) -> Matrix ns a -> Element (Matrix ns a) # minimumByEx :: (Element (Matrix ns a) -> Element (Matrix ns a) -> Ordering) -> Matrix ns a -> Element (Matrix ns a) # | |
type Rep (Matrix ns) Source # | |
Defined in Termonad.Config.Vec | |
type Element (Matrix ns a) Source # | |
Defined in Termonad.Config.Vec |
data MatrixTFSym1 (ns :: [Peano]) (z :: TyFun Type Type) Source #
forall (arg :: Type).SameKind (Apply (MatrixTFSym1 ns) arg) (MatrixTFSym2 ns arg) => MatrixTFSym1KindInference |
data MatrixTFSym0 (l :: TyFun [Peano] (Type ~> Type)) Source #
forall (arg :: [Peano]).SameKind (Apply MatrixTFSym0 arg) (MatrixTFSym1 arg) => MatrixTFSym0KindInference |
Instances
type Apply MatrixTFSym0 (l :: [Peano]) Source # | |
Defined in Termonad.Config.Vec |
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 #
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 #