Libraries.Data.List.LengthMatch

Definitions

data LengthMatch : List a -> List b -> Type

Totality: total
Visibility: public export
Constructors:

NilMatch : LengthMatch [] []

ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)

checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)

Totality: total
Visibility: export

lengthsMatch : LengthMatch xs ys -> length xs = length ys

Totality: total
Visibility: export