Nikola Katić (Aug 16 2022 at 04:10): 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?
Paolo Giarrusso (Aug 16 2022 at 09:49):What exactly did the notation look without them? Because you’re right, those parts are problematic.
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]).
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: Oct 13 2024 at 01:02 UTC