Skip to content

Instantly share code, notes, and snippets.

@Ralith
Created July 6, 2012 03:05
Show Gist options
  • Save Ralith/3057830 to your computer and use it in GitHub Desktop.
Save Ralith/3057830 to your computer and use it in GitHub Desktop.
Working dependent maybeZip
module main
list1 : List Int
list1 = [1, 2, 3]
list2 : List Int
list2 = [4,5,6]
total equalLen : (xs : List a) -> (ys : List b) -> Maybe (length xs = length ys)
equalLen [] [] = Just refl
equalLen (x::xs) (y::ys) = fmap cong $ equalLen xs ys
equalLen _ _ = Nothing
maybeZip : List a -> List b -> Maybe (List (a,b))
maybeZip xs ys = fmap (\p => zip xs ys p) (equalLen xs ys)
main : IO ()
main = print . show $ maybeZip list1 list2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment