coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Paul Tarau <paul.tarau AT gmail.com>
- To: brandon_m_moore AT yahoo.com
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] applying a function definition
- Date: Mon, 27 Jun 2011 13:44:10 -0500
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=w9787lAdXsh6rby7onY+gB8t3kD0ImXhcPqxsj0kS2bnuc74HesZF/WfaqnJhqWB2X GgWKfM32rWnQTVI3UoI0IEAZjfmaHtVLCNOsAXh0baAuIDJarQjsMvkl+ehu8I5REiqm MVXqAEpcE3UrAVz8x6iJBeeV41KEauWyBVH00=
Thanks a lot - it does work indeed! And this typo proves that humans and not
Coq are the usual suspects :-)
The most interesting challenge now is to prove that the borrowedS and
borrowedP successor/predecessor functions are equivalent to sT and pT.
I was wondering if anyone has seen papers about taking advantage of the
presence of a bijection between some trickier data type and "nat" to somewhat
automate the proof of computations or properties borrowed from "nat" using
the bijection. Or papers about automation of structural recursion
requirements in the presence of such a bijection.
Paul
On Jun 27, 2011, at 1:27 PM,
brandon_m_moore AT yahoo.com
wrote:
> The code seems to work correctly after replacing
>
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C _ y =>y
> end.
>
> by
>
> Definition hdT (a:T) : T :=
> match a with
> | E => E
> | C x _ =>x
> end.
- Re: [Coq-Club] applying a function definition, Paul Tarau
- Re: [Coq-Club] applying a function definition, Andreas Abel
- Re: [Coq-Club] applying a function definition,
AUGER Cedric
- Re: [Coq-Club] applying a function definition,
Paul Tarau
- Re: [Coq-Club] applying a function definition, Paul Tarau
- Re: [Coq-Club] applying a function definition,
Paul Tarau
- <Possible follow-ups>
- Re: Re: [Coq-Club] applying a function definition,
brandon_m_moore
- Re: [Coq-Club] applying a function definition, Paul Tarau
Archive powered by MhonArc 2.6.16.