Skip to content

Instantly share code, notes, and snippets.

/map2gen.v

Created August 26, 2013 19:53
Show Gist options
  • Save anonymous/6345872 to your computer and use it in GitHub Desktop.
Save anonymous/6345872 to your computer and use it in GitHub Desktop.
Download ZIP
generalize map2 for ilist
Raw
map2gen.v
Fixpoint map2gen {A B C n} (f : A -> B -> C) (xs : ilist A n) : ilist B n -> ilist C n :=
match xs in ilist _ n return ilist B n -> ilist C n with
| INil => fun _ => INil
| ICons n' x xs' => fun ys => ICons (f x (hd ys)) (map2gen f xs' (tl ys))
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment