Libraries.Data.SnocList.LengthMatch

Definitions

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

Totality: total
Visibility: public export
Constructors:

LinMatch : LengthMatch [<] [<]

SnocMatch : LengthMatch xs ys -> LengthMatch (xs :< x) (ys :< y)

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

reverseOnto : LengthMatch sx sy -> LengthMatch sx' sy' -> LengthMatch (reverseOnto sx sx') (reverseOnto sy sy')

Totality: total
Visibility: export

reverse : LengthMatch sx sy -> LengthMatch (reverse sx) (reverse sy)

Totality: total
Visibility: export