Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/safe_head.v

Last active August 29, 2015 14:10
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 gallais/aa0aaad9edbc9e361eb2 to your computer and use it in GitHub Desktop.
Save gallais/aa0aaad9edbc9e361eb2 to your computer and use it in GitHub Desktop.
Download ZIP
Safe Head
Raw
safe_head.v
Inductive Vector (A : Type) : nat -> Type :=
| nil : Vector A O
| cons : forall n, A -> Vector A n -> Vector A (S n).
Definition head (A : Type) (n : nat) (v : Vector A (S n)) : A.
refine (
(match v in Vector _ m return m = S n -> A with
| nil => _
| cons _ hd tl => fun _ => hd
end) (eq_refl (S n))).
inversion 1.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment