coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Parameters in "Definitions"?

From: "Randy Pollack" <rap AT dcs.ed.ac.uk>
To: Bruno.Barras AT cl.cam.ac.uk
Cc: coq-club AT pauillac.inria.fr, Bruno.Barras AT cl.cam.ac.uk
Subject: Re: Parameters in "Definitions"?
Date: Mon, 15 Feb 1999 18:27:29 GMT

Hi Bruno,

rap> The notation I want almost exists, by using a Fixpoint with a dummy
rap> boolean argument.

barras> I don't understand why you need this extra argument...

I was misled by the manual (p.35) which says the type of the recursive
variable should be inductively defined. I was using a dummy boolean
just to have some inductive argument.

Still, it would be better to make "Definition" accept parameters.

Thanks,
Randy

Parameters in "Definitions"?, Randy Pollack
- Re: Parameters in "Definitions"?, Bruno Barras
  - Re: Parameters in "Definitions"?, Randy Pollack
    - Re: Parameters in "Definitions"?, Patrick Loiseleur