Documentation

assocThm :: forall a b c. ((a ++ b) ++ c) :~: (a ++ (b ++ c)) Source #

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 #

pairNExtensionThm :: forall s a n. ((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength a n ~ 'True) => PeanoNatural n -> Dict (ConstraintPairN n (a ++ s), RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a), Drop n (a ++ s) ~ (Drop n a ++ s)) Source #

unpairNExtensionThm :: forall s a b n x r. (a ~ (x : r), CombedPairLeafCountIsAtLeast n x ~ 'True, (n >= ToPeano 2) ~ 'True, (UnpairN n x ++ r) ~ b) => PeanoNatural n -> Dict (ConstraintUnpairN n x, (UnpairN n x ++ (r ++ s)) ~ (b ++ s)) Source #