The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you have a particular broken notation, you can debug it by making the following straightforward transformation:

Require Import String.                                                                   

Local Open Scope string_scope.                                                           

Notation "'bFoo' A 'eFoo'" := (A, "+", 2) (only parsing).                                

                                                                                         

Eval simpl in (bFoo 2 eFoo).                                                             

                                                                                         

Eval simpl in (bFoo false eFoo).

I don't know of a good way to do this automatically.

Alternatively, you could protect all of your variables with evars, e.g.,

  Eval simpl in bFoo (_ false) eFoo

and then mentally discard all the ?n. (And, again, the (only parsing) annotation is your friend here.)

-Jason

On Wednesday, August 28, 2013, t x wrote:

Consider the following minimal failure example:

Notation "'bFoo' A 'eFoo'" := (A + 2).

Eval simpl in (bFoo 2 eFoo).

Eval simpl in (bFoo false eFoo).

Right now, all I get is: a complaint of "got bool while expectig Z"

This is not particularly useful on larger examples.

The process appears to be:

[1] (bFoo false eFoo)

[2] (false + 2)

[3] type-check

[4] report type check error

Is there a way to put in a [2.5] --> print out what _expression_ is, before it is type checked?

Seeing "(false + 2)" would make debugging much easier than just a "got bool; expected Z"

Thanks!