coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 'Eval ... in' in type declarations.

From: Marco Maggesi <maggesi AT hermes.math.unifi.it>
To: Coq Club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] 'Eval ... in' in type declarations.
Date: Tue, 27 May 2003 19:53:55 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq Club,

'Eval ... in' it is not recognized in type declarations.  Example:

  Syntactic Definition ASSOC := [A:Type; mul:A->A->A]
    (x,y,z:A) (mul x (mul y z))=(mul (mul x y) z) | 1.

  Record Magma : Type := {
    carrier :> Type;
    mul : carrier->carrier->carrier;
    assoc : Eval Simpl in (ASSOC mul)
   }.

  Syntax error: '}' expected after [fields] (in [vernac:gallina_ext])

Is it possible to correct this?  Are there technical reasons that make
this difficult?

Thanks

  -- Marco

[Coq-Club] 'Eval ... in' in type declarations., Marco Maggesi