Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Module, containing some internally used typelevel proofs.
Documentation
takeExtensionThm :: forall a s n. IsLongerOrSameLength a n ~ 'True => PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a Source #
dropExtensionThm :: forall a s n. IsLongerOrSameLength a n ~ 'True => PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s) Source #
isLongerOrSameLengthExtThm :: forall a s n. IsLongerOrSameLength a n ~ 'True => PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True Source #
isLongerOrSameLengthDecThm :: forall a m. IsLongerOrSameLength a ('S m) ~ 'True => PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True Source #
isLongerThanExtThm :: forall a s n. IsLongerThan a n ~ 'True => PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True Source #
dropHeadThm :: forall x a n. IsLongerThan (x : a) n ~ 'True => PeanoNatural n -> IsLongerOrSameLength a n :~: 'True Source #
isLongerThanIncThm :: forall a n. IsLongerThan a n ~ 'True => PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True Source #
dugLengthThm :: forall b x n. IsLongerThan b n ~ 'True => PeanoNatural n -> IsLongerThan (x ': (LazyTake n b ++ Drop ('S n) b)) n :~: 'True Source #
dropNExtensionThm :: forall s a b n. (Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) => PeanoNatural n -> Dict (Drop n (a ++ s) ~ (b ++ s), IsLongerOrSameLength (a ++ s) n ~ 'True) Source #
dupNExtensionThm :: forall s a b n x. ConstraintDUPN n a b x => PeanoNatural n -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x) Source #
dugNExtensionThm :: forall s a b x r n. (a ~ (x : r), ConstraintDUG n a b x) => PeanoNatural n -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x) Source #
digNExtensionThm :: forall s a b x r n. (b ~ (x : r), ConstraintDIG n a b x) => PeanoNatural n -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x) Source #
dipNExtensionThm :: forall s a b s1 s1' n. ConstraintDIPN n a b s1 s1' => PeanoNatural n -> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s)) Source #
dipNExtensionLemma :: forall inp out s n. (RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) => PeanoNatural n -> IsLongerOrSameLength out n :~: 'True Source #