The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

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.)

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?

  Tom