Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question on Opaque/Transparent... or: one step of reduction of a fixpoint

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question on Opaque/Transparent... or: one step of reduction of a fixpoint


chronological Thread 
  • From: "AUGER Cédric" <sedrikov AT gmail.com>
  • To: Stéphane Glondu <steph AT glondu.net>
  • Cc: Francois Pottier <Francois.Pottier AT inria.fr>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Question on Opaque/Transparent... or: one step of reduction of a fixpoint
  • Date: Mon, 27 Feb 2012 19:30:11 +0100
  • Authentication-results: mr.google.com; spf=pass (google.com: domain of sedrikov AT gmail.com designates 10.180.78.233 as permitted sender) smtp.mail=sedrikov AT gmail.com; dkim=pass header.i=sedrikov AT gmail.com
Le Mon, 27 Feb 2012 18:12:17 +0100,
Stéphane Glondu 
<steph AT glondu.net>
 a Ã©crit :

> Le 27/02/2012 13:53, Francois Pottier a Ã©crit :
> > What I would like to do at this point is perform one step of
> > reduction, that is, reduce the application of f to (C x) by
> > appealing to the definition of f as a Fixpoint.
> 
> Not exactly what you're asking for, but what about "unfold f; fold f"?
> 
> 
> Cheers,
> 

If it is some very precise place, you can also consider
"change f with (C x) [in â€¦] [at â€¦]."

The "fold" is often not what I want (I have to give the parameters of
"f", like in "fold (f x)." to do what I want), but in case of
fixpoint, Stéphane suggestion should work if there is no
automatic reduction inside the fixpoint definition (which hopefully
shouldn't occur).


Archive powered by MhonArc 2.6.16.

Top of Page