coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Local Fixpoint definitions?

From: Jean-Christophe Filliatre <filliatr AT lri.fr>
To: "Randy Pollack" <rap AT dcs.ed.ac.uk>
Cc: coq AT pauillac.inria.fr, coq-club AT pauillac.inria.fr
Subject: Re: Local Fixpoint definitions?
Date: Thu, 13 May 1999 23:00:52 +0200 (MET DST)

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

Use Local and Fix (instead of Fixpoint, which is a combination of
Definition and Fix) i.e.

  Local f := Fix f { f/1 : ... := ... }.

Best regards,
--
Jean-Christophe FILLIATRE

mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr

Local Fixpoint definitions?, Randy Pollack
- Re: Local Fixpoint definitions?, Jean-Christophe Filliatre
- Re: Local Fixpoint definitions?, Patrick Loiseleur