coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Equality for inductive type containing list
- Date: Thu, 06 Oct 2016 16:29:58 +0200
- Organization: LORIA
On 10/06/2016 04:18 PM, Klaus Ostermann wrote:
> Hi Dominque
>
> thanks a lot! Your solution works like a charm. Very nice!
>
> That said, I'm fascinated how much work is required to do something
> so basic.
>
> In general, my impression as a Coq beginner is that is relatively easy to
> follow one of the numerous Coq tutorials and solve the exercises, but
> as soon as you try to do something yourself, you run into many complicated
> pitfalls that the exercise designers have carefully avoided.
This is very true.
I did not know that it was possible to parametrize the decide equality
tactic as Clément showed. Since obviously, decide equality cannot
rely on the Coq generated inductive principle ty_rec (ty_rec is too
weak), it must find one itself.
So I wonder why the nested induction required by the type of trees ty
is still not guessed when Coq generates induction principles.
Dominique
- [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Clément Pit--Claudel, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Abhishek Anand, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Jonathan Leivent, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
Archive powered by MHonArc 2.6.18.