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]).
110 at random, after experimenting with different levels (with no success of getting rid of the message).
It seemed to me that
, were problematic parts, but even without them message persisted.
What is causing the message in this scenario?
What exactly did the notation look without them? Because you’re right, those parts are problematic.
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: Sep 23 2023 at 07:01 UTC