The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/17/2015 09:42 PM, Jason Gross wrote:
> Notation get' n x := $(let ret := constr:(_ : get n x) in let ret' := (eval
> hnf in ret) in exact ret')$.
>
> (your body works too).

I actually need a function, not the mere appearance of a function.

However, I found an easier alternative - if I use a hetero list that 
specifies its element types as a list Type, then the get function (hnth) 
is very easy to write (at least in proof mode), no typeclasses needed:

Require Import List.
Import ListNotations.

Inductive hlist : list Type -> Type :=
| hnil : hlist nil
| hcons{A B}(a : A)(b : hlist B) : hlist (A::B).

Definition hnth : forall {l}(n : nat)(h : hlist l), nth n l unit.
Proof.
induction l; intros [|] h; cbn; inversion h; auto using tt.
Defined.

Yes, it's a list and not a tuple - but that's not a big deal.

-- Jonathan