Skip to content

Instantly share code, notes, and snippets.

@mak
Created April 11, 2010 16:00
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mak/362840 to your computer and use it in GitHub Desktop.
Save mak/362840 to your computer and use it in GitHub Desktop.
Inductive vector (A:Set) : nat -> Type :=
| vnil : vector A 0
| vcons : forall n, A -> vector A n -> vector A (S n).
Implicit Arguments vector [A].
Implicit Arguments vcons [A n].
Implicit Arguments vnil [A].
Fixpoint vecfold (A:Set) B n (f : A -> B -> B) (c:B) (l:vector n) :=
match l with
| vnil => c
| vcons n0 x xs => f x (vecfold A B n0 f c xs)
end.
Implicit Arguments vecfold [A B n].
Set Implicit Arguments.
Print vecfold.
Eval compute in (vecfold (fun x y => x + y) 0 (vcons 1 (vcons 2 vnil))).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment