Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Having trouble understanding a proof term generated by fix

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Having trouble understanding a proof term generated by fix


chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • Cc: AUGER Cedric <Cedric.Auger AT lri.fr>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Having trouble understanding a proof term generated by fix
  • Date: Sun, 24 Apr 2011 11:16:58 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:cc:references:in-reply-to :mime-version:content-type:content-transfer-encoding:message-id; b=WGxjeJIm9T3/Sz7Ckz3onVXSr0nUnXKpmDIW/w4teujOFv2saMSo9Spmu615KFydfL osFIeRR5FSJcyosMFV98GJlbrKPdaWgeGsBkLF85YjKTd+JRTgXERDhibpH/SC1/QtPN b127/3m0z9w03woWP+o1eMbEHPZ2ehwq9X8Rc=
On Sunday 24 April 2011 05:49:17 Hugo Herbelin wrote:

> fix Pind2 {struct p}
> 
>     := fun P H1 Hind (H:=...) p => match ... with ... end
>     :
>     :  forall P, P 1 -> (forall p, P p -> P (Psucc p)) -> forall p, P p

By this do you mean

fix Pind2 {struct p}
  := fun P H1 Hind =>
  let H:=... in
  fun p => match ... end
  : forall P, ...
?

That would make sense in terms of the proof script I originally wrote.
-- 
Daniel Schepler

Archive powered by MhonArc 2.6.16.

Top of Page