
  0 | module Libraries.Data.SnocList.LengthMatch
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | data LengthMatch : SnocList a -> SnocList b -> Type where
  6 |      LinMatch : LengthMatch [<] [<]
  7 |      SnocMatch : LengthMatch xs ys -> LengthMatch (xs :< x) (ys :< y)
  8 | 
  9 | export
 10 | checkLengthMatch : (xs : SnocList a) -> (ys : SnocList b) ->
 11 |   Maybe (LengthMatch xs ys)
 12 | checkLengthMatch [<] [<] = Just LinMatch
 13 | checkLengthMatch [<] (_ :< _) = Nothing
 14 | checkLengthMatch (_ :< _) [<] = Nothing
 15 | checkLengthMatch (xs :< _) (ys :< _)
 16 |     = Just (SnocMatch !(checkLengthMatch xs ys))
 17 | 
 18 | export
 19 | lengthsMatch : LengthMatch xs ys -> (length xs) = (length ys)
 20 | lengthsMatch LinMatch = Refl
 21 | lengthsMatch (SnocMatch x) = cong S (lengthsMatch x)
 22 | 
 23 | export
 24 | reverseOnto : LengthMatch sx sy -> LengthMatch sx' sy' ->
 25 |   LengthMatch (reverseOnto sx sx') (reverseOnto sy sy')
 26 | reverseOnto p LinMatch = p
 27 | reverseOnto p (SnocMatch x) = reverseOnto (SnocMatch p) x
 28 | 
 29 | export
 30 | reverse : LengthMatch sx sy -> LengthMatch (reverse sx) (reverse sy)
 31 | reverse = reverseOnto LinMatch
 32 |