ox-arrays-0.1.0.0: An efficient CPU-based multidimensional array (tensor) library
Safe HaskellNone
LanguageHaskell2010

Data.Array.Nested.Lemmas

Synopsis

Lemmas about numbers and lists

Nat

lemLeqSuccSucc :: forall (k :: Natural) (n :: Natural). (k + 1) <= n => Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True Source #

lemLeqPlus :: forall (n :: Natural) (m :: Natural) (k :: Natural). n <= m => Proxy n -> Proxy m -> Proxy k -> (n <=? (m + k)) :~: 'True Source #

Append

lemAppNil :: forall {a} (l :: [a]). (l ++ ('[] :: [a])) :~: l Source #

lemAppAssoc :: forall {a1} (a2 :: [a1]) (b :: [a1]) (c :: [a1]). Proxy a2 -> Proxy b -> Proxy c -> ((a2 ++ b) ++ c) :~: (a2 ++ (b ++ c)) Source #

lemAppLeft :: forall {a1} (l :: [a1]) (a2 :: [a1]) (b :: [a1]). Proxy l -> (a2 :~: b) -> (a2 ++ l) :~: (b ++ l) Source #

Simple type families

lemReplicatePlusApp :: forall {a1} (n :: Nat) (m :: Natural) (a2 :: a1). SNat n -> Proxy m -> Proxy a2 -> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2) Source #

lemDropLenApp :: forall {a1} {a} (l1 :: [a1]) (l2 :: [a]) (rest :: [a]). Rank l1 <= Rank l2 => Proxy l1 -> Proxy l2 -> Proxy rest -> (DropLen l1 l2 ++ rest) :~: DropLen l1 (l2 ++ rest) Source #

lemTakeLenApp :: forall {a1} {a} (l1 :: [a1]) (l2 :: [a]) (rest :: [a]). Rank l1 <= Rank l2 => Proxy l1 -> Proxy l2 -> Proxy rest -> TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest) Source #

lemInitApp :: forall {a} (l :: [a]) (x :: a). Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l Source #

lemLastApp :: forall {k} (l :: [k]) (x :: k). Proxy l -> Proxy x -> Last (l ++ '[x]) :~: x Source #

KnownNat

lemKnownNatSucc :: forall (n :: Nat). KnownNat n => Dict KnownNat (n + 1) Source #

lemKnownNatRank :: forall (sh :: [Maybe Nat]) i. ShX sh i -> Dict KnownNat (Rank sh) Source #

lemKnownNatRankSSX :: forall (sh :: [Maybe Nat]). StaticShX sh -> Dict KnownNat (Rank sh) Source #

Lemmas about shapes

Known shapes

lemKnownShX :: forall (sh :: [Maybe Nat]). StaticShX sh -> Dict KnownShX sh Source #

lemKnownMapJust :: forall (sh :: [Nat]). KnownShS sh => Proxy sh -> Dict KnownShX (MapJust sh) Source #

Rank

lemRankApp :: forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]). StaticShX sh1 -> StaticShX sh2 -> Rank (sh1 ++ sh2) :~: (Rank sh1 + Rank sh2) Source #

lemRankAppComm :: forall {a} proxy (sh1 :: [a]) (sh2 :: [a]). proxy sh1 -> proxy sh2 -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1) Source #

lemRankReplicate :: forall proxy (n :: Natural). proxy n -> Rank (Replicate n ('Nothing :: Maybe Nat)) :~: n Source #

lemRankMapJust :: forall (sh :: [Nat]). ShS sh -> Rank (MapJust sh) :~: Rank sh Source #

Related to MapJust and/or Permutation

lemTakeLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> TakeLen is (MapJust sh) :~: MapJust (TakeLen is sh) Source #

lemDropLenMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> DropLen is (MapJust sh) :~: MapJust (DropLen is sh) Source #

lemIndexMapJust :: forall (i :: Nat) (sh :: [Nat]). SNat i -> ShS sh -> Index i (MapJust sh) :~: 'Just (Index i sh) Source #

lemPermuteMapJust :: forall (is :: [Nat]) (sh :: [Nat]). Perm is -> ShS sh -> Permute is (MapJust sh) :~: MapJust (Permute is sh) Source #

lemMapJustApp :: forall (sh1 :: [Nat]) (sh2 :: [Nat]). ShS sh1 -> Proxy sh2 -> MapJust (sh1 ++ sh2) :~: (MapJust sh1 ++ MapJust sh2) Source #