coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Parsing "Fixpoint".

From: "Randy Pollack" <rap AT dcs.ed.ac.uk>
To: coq AT pauillac.inria.fr, coq-club AT pauillac.inria.fr, Bruno.Barras AT cl.cam.ac.uk
Subject: Parsing "Fixpoint".
Date: Mon, 15 Feb 1999 19:23:37 GMT

  Coq < Fixpoint test [a:Prop][b:Set] : Set := b.
  Toplevel input, characters 23-24
  > Fixpoint test  [a:Prop][b:Set] : Set := b.
  >                        ^
  Syntax error: ':' expected after ']' (in [Vernac.onerec])

  Coq < Fixpoint test [a:Prop;b:Set] : Set := b.
  Warning: test is non-recursively defined

You probably don't consider this a bug, but if "[a:Prop][b:Set]" and
"[a:Prop;b:Set]" mean the same thing, why can't they both be parsed?

Randy

Parsing "Fixpoint"., Randy Pollack
- Re: Parsing "Fixpoint"., Patrick Loiseleur