Skip to content

Instantly share code, notes, and snippets.

@wilcoxjay

wilcoxjay/akr_fold.v

Created August 3, 2016 17:29
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save wilcoxjay/402e162e4af412ad0ce0c8603987173c to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save wilcoxjay/402e162e4af412ad0ce0c8603987173c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
akr_fold.v
Require Import List.
Import ListNotations.
Fixpoint akr_fold {A} (P : nat -> Type) (P_nil : P 0) (P_cons : forall n, A -> P n -> P (S n)) (l : list A) : P (length l) :=
match l with
| [] => P_nil
| a :: l' => P_cons _ a (akr_fold P P_nil P_cons l')
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment