module Data.LengthMatch public exportdata LengthMatch : List a -> List b -> Type where NilMatch : LengthMatch [] [] ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys) exportcheckLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)checkLengthMatch [] [] = Just NilMatchcheckLengthMatch [] (x :: xs) = NothingcheckLengthMatch (x :: xs) [] = NothingcheckLengthMatch (x :: xs) (y :: ys) = Just (ConsMatch !(checkLengthMatch xs ys))
module Data.LengthMatch
public export
data LengthMatch : List a -> List b -> Type where
NilMatch : LengthMatch [] []
ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
export
checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
checkLengthMatch [] [] = Just NilMatch
checkLengthMatch [] (x :: xs) = Nothing
checkLengthMatch (x :: xs) [] = Nothing
checkLengthMatch (x :: xs) (y :: ys)
= Just (ConsMatch !(checkLengthMatch xs ys))