coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/15/2015
- Re: [Coq-Club] heterogeneous tuple element function, Vilhelm Sjöberg, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Vilhelm Sjöberg, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, flicky frans, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Vilhelm Sjöberg, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jason Gross, 01/17/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/17/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jason Gross, 01/18/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/18/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/17/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jason Gross, 01/17/2015
- Re: [Coq-Club] heterogeneous tuple element function, flicky frans, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Vilhelm Sjöberg, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] heterogeneous tuple element function, Vilhelm Sjöberg, 01/16/2015
Archive powered by MHonArc 2.6.18.