The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

In his message from Thursday 13 May, 1999, Randy Pollack wrote: 
> How can Fixpoint definitions be made local in the sense that "Local"
> makes definitions local and "Remark" makes lemmas local?
> 
> Randy

You must use "Local" that creates local constants and "Fix" that
creates anonymous (mutual) fixpoints. Here is an example:

Local plus := Fix toto {toto[n:nat]: nat -> nat :=
                   [m:nat]Cases n of 
                   |    O => m
                   |    (S n') => (S (toto n' m))
                   end}.

I used "toto" here to demonstrate that this is a bound name and so its
value is irrelevant. But you might want to call it "plus".

Maybe it would be a good idea to add a "Local Fixpoint" command,
symmetric of "Local" w.r.t. "Definition" or "Remark" w.r.t "Theorem".

Best regards,

Patrick

-- 
Patrick.Loiseleur AT lri.fr