Documentation

dropNDropNProof :: forall inp out out' n m. (out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True, out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) => PeanoNatural n -> PeanoNatural m -> Dict (Drop (AddPeano n m) inp ~ out', IsLongerOrSameLength inp (AddPeano n m) ~ 'True) Source #

unpairN2isUnpairProof :: forall inp out pair s. (inp ~ (pair : s), out ~ (UnpairN ('S ('S 'Z)) pair ++ s), ConstraintUnpairN (ToPeano 2) pair) => inp :~: PairN (ToPeano 2) out Source #

unpairNisUnpairDipUnpairNProof :: forall inp out pair s n. (inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s), ConstraintUnpairN ('S n) pair) => PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out) Source #

dipPairNPairIsPairNProof :: forall inp n. ((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength (Tail inp) n ~ 'True, inp ~ (Head inp : Tail inp)) => PeanoNatural n -> PairN ('S n) inp :~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp))) : Drop n (Tail inp)) Source #

pairN2isPairProof :: forall inp. IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True => inp :~: (Head inp : (Head (Tail inp) : Drop ('S ('S 'Z)) inp)) Source #

unconsListProof :: forall inp n. IsLongerOrSameLength inp ('S n) ~ 'True => PeanoNatural n -> inp :~: (Head inp : Tail inp) Source #