Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/fold_rightに関する未解決問題.v

Created July 29, 2017 12:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 2 You must be signed in to fork a gist
  • Save yoshihiro503/701310ab65b1f34bfc369997a5f00cb1 to your computer and use it in GitHub Desktop.
Save yoshihiro503/701310ab65b1f34bfc369997a5f00cb1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
fold_rightに関する未解決問題.v
Require Import Program.
Open Scope list_scope.
Lemma fold_right_tail : forall (A B: Type) (f: A -> B -> B) xs x b0,
List.fold_right f b0 (xs ++ [x]) = List.fold_right f (f x b0) xs.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment