The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You don't need Ltac2 for this.  The trick is to bind x to a different name in Gallina, eg,

Notation "'[SIMPL]' x" := (match x with y => ltac:(let x := eval cbv delta y in y in idtac x; let x := eval simpl in x in exact x) end)

  (only parsing, at level 0, x at level 200).

On Mon, Mar 23, 2020, 21:58 Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

I'm trying to write a notation that simplifies its argument. I wrote the following:

Notation "'[SIMPL]' x" := (ltac:(idtac x; let x := eval simpl in x in exact x))

  (only parsing, at level 0, x at level 200).

Definition foo := [SIMPL] 1 + 1.
Print foo. (* := 2 *)

Unfortunately, if there is an unbound identifier in the argument of [SIMPL], I get an error message saying "x not found". What I want to do, is perform the type checking, and get the usual error message if there is an error, and otherwise, reduce the term and exact the result. I was wondering if there is some way that I could do this with Ltac2, but I haven't been able to figure it out.

I know that if I'm defining a term, I can write something like:

Definition foo := Eval simpl in 1 + 1.

but I can't seem to do the same thing at the type level, e.g.

Definition foo : Eval simpl in 1 + 1 = 1 + 1.

Any pointers or suggestions would be greatly appreciated.

Thanks.

--

gregory malecha

gmalecha.github.io