Math.VectorSpace.DimensionAware.Theorems.MaybeNat

Description

Documentation

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

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 ... Source #

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 ... Source #

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 ... Source #

Equations

MaybePred 0 = 'Nothing
MaybePred n = 'Just (n - 1)

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

Equations

BindMaybePred 'Nothing = 'Nothing
BindMaybePred ('Just n) = MaybePred n

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

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

Equations

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

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