
  0 | module Libraries.Data.List.LengthMatch
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | data LengthMatch : List a -> List b -> Type where
  6 |      NilMatch : LengthMatch [] []
  7 |      ConsMatch : LengthMatch xs ys -> LengthMatch (x :: xs) (y :: ys)
  8 | 
  9 | export
 10 | checkLengthMatch : (xs : List a) -> (ys : List b) -> Maybe (LengthMatch xs ys)
 11 | checkLengthMatch [] [] = Just NilMatch
 12 | checkLengthMatch [] (x :: xs) = Nothing
 13 | checkLengthMatch (x :: xs) [] = Nothing
 14 | checkLengthMatch (x :: xs) (y :: ys)
 15 |     = Just (ConsMatch !(checkLengthMatch xs ys))
 16 | 
 17 | export
 18 | lengthsMatch : LengthMatch xs ys -> (length xs) = (length ys)
 19 | lengthsMatch NilMatch = Refl
 20 | lengthsMatch (ConsMatch x) = cong (S) (lengthsMatch x)
 21 |