The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Sat, 2012-04-07 at 11:17 -0400, Tom Prince wrote:
> On Sat, 7 Apr 2012 02:36:55 +0200, Bernard 
> Hurley<bernard AT marcade.biz>
>  wrote:
> > Is it possible to get the effect of a Local prefix with Fixpoint.  I 
> > searched
> > the email archive but the solution I found (from 1999) doesn't work with 
> > the
> > current version of coq.
> 
> I'm not sure what behavior you expect from something like 'Local
> Fixpoint'. 'Local' typically only applies to options or tactic database
> settings. (When used with 'Instance', for example, it doesn't cuase the
> definition to disappear at the end of the block, only the assoicated
> hint.)
> 

Thanks, I have only been using coq for a couple of weeks, so I'm only
just getting used to what it's all about.

> The only method of creating a local definition is with 'Let', which
> causes the definition to be turned into a 'let ... in ...' when the
> section is closed. You can create annonymous fixpoints, using 'fix', and
> then bind them with 'Let', but I'm not sure if this is actually what you
> want to use.
> 
> What is your use case?

I didn't have a use case in mind I'm just trying to learn what the
system can do.

Bernard.