Math.VectorSpace.DimensionAware.Theorems.MaybeNat

Documentation

type family ZipWith (f :: k -> l -> m) (a :: Maybe k) (b :: Maybe l) :: Maybe m where ...

Equations

ZipWith f 'Nothing y = 'Nothing

ZipWith f x 'Nothing = 'Nothing

ZipWith f ('Just x) ('Just y) = 'Just (f x y)

type family ZipWithPlus (a :: Maybe Nat) (b :: Maybe Nat) :: Maybe Nat where ...

Equations

ZipWithPlus 'Nothing y = 'Nothing

ZipWithPlus x 'Nothing = 'Nothing

ZipWithPlus ('Just x) ('Just y) = 'Just (x + y)

type family ZipWithTimes (a :: Maybe Nat) (b :: Maybe Nat) :: Maybe Nat where ...

Equations

ZipWithTimes 'Nothing y = 'Nothing

ZipWithTimes x 'Nothing = 'Nothing

ZipWithTimes ('Just x) ('Just y) = 'Just (x * y)

type family MaybePred (a :: Nat) :: Maybe Nat where ...

Equations

MaybePred 0 = 'Nothing

MaybePred n = 'Just (n - 1)

type family BindMaybePred (a :: Maybe Nat) :: Maybe Nat where ...

Equations

BindMaybePred 'Nothing = 'Nothing

BindMaybePred ('Just n) = MaybePred n

type TriangularNum (a :: Nat) = (a * (a + 1)) `Div` 2

type family FmapTriangularNum (a :: Maybe Nat) where ...

Equations

FmapTriangularNum 'Nothing = 'Nothing

FmapTriangularNum ('Just n) = 'Just (TriangularNum n)

justNatSing :: forall (n :: Nat). Sing n -> Sing ('Just n)

succMaybePredSing :: forall n. SNat n -> Sing (MaybePred (n + 1))

maybePredSing :: forall a. Sing a -> Sing (MaybePred a)

binMaybePredSing :: forall a. Sing a -> Sing (BindMaybePred a)

triangularNumSing :: forall a. Sing a -> Sing (TriangularNum a)

fmapTriangularNumSing :: forall a. Sing a -> Sing (FmapTriangularNum a)

zipWithPlusSing :: forall a b r. Sing a -> Sing b -> Sing (ZipWithPlus a b)

zipWithTimesSing :: forall a b r. Sing a -> Sing b -> Sing (ZipWithTimes a b)

zipWithTimesAssoc :: forall a b c r. Sing a -> Sing b -> Sing c -> (ZipWithTimes a (ZipWithTimes b c) ~ ZipWithTimes (ZipWithTimes a b) c => r) -> r

zipWithTimesCommu :: forall a b r. Sing a -> Sing b -> (ZipWithTimes a b ~ ZipWithTimes b a => r) -> r