Stream: Coq users

Topic: Choosing notation level


view this post on Zulip Nikola Katić (Aug 16 2022 at 04:10):

Hi all,
When creating a relation, I've added this notation layer:

Reserved Notation "'(' env ',' exps ',' s1 ')' '==>' '(' vs ',' s2 ')'"
  (at level 110).

Very often, when coding other stuff, this error message pops up:
Error: Syntax error: ',' expected after [term level 200] (in [term]).

I put 110 at random, after experimenting with different levels (with no success of getting rid of the message).
It seemed to me that (, ) and , were problematic parts, but even without them message persisted.

What is causing the message in this scenario?

view this post on Zulip Paolo Giarrusso (Aug 16 2022 at 09:49):

What exactly did the notation look without them? Because you’re right, those parts are problematic.

view this post on Zulip Nikola Katić (Aug 16 2022 at 10:49):

Well, I tried multiple combinations (with or without certain characters) and forgot that having it like this:

Reserved Notation "env exps s1 '==>' vs s2" (at level 110).
Inductive evalR : env -> list exp -> state -> list val -> state -> Prop :=
| E_Const (e : env) (n : nat) (s : state) :
  e [Const n] s ==> [VNum n] s
where "env exps s1 '==>' vs s2" := (evalR env exps s1 vs s2).

stopped me from being able to step through it:

Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).

view this post on Zulip Nikola Katić (Aug 16 2022 at 12:27):

For anyone who might be in similar situation -- this seems not to produce any aforementioned issues:

Reserved Notation "l '==>' r" (at level 110).
Inductive evalR : (env * (list exp) * state) -> ((list val) * state) -> Prop :=
| E_Const (e : env) (n : nat) (s : state) :
  (e, [Const n], s) ==> ([VNum n], s)
where "l '==>' r" := (evalR l r).

Last updated: Jan 27 2023 at 01:03 UTC