Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] heterogeneous tuple element function

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] heterogeneous tuple element function


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] heterogeneous tuple element function
  • Date: Sat, 17 Jan 2015 23:15:06 -0500


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




Archive powered by MHonArc 2.6.18.

Top of Page