CODEWITHSUNDEEP
coq
aqjune
aqjune

Reputation: 552

Coq "Unknown interpretation for notation" error

I'm following instructions in https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html, and trying to define a new notation |\. (Instead of ||, which is used in the webpage but seems to be interpreted as an OR operator by my coq)

Reserved Notation "e |\ n" (at level 50, left associativity).

However coq still thinks that |\ is an undefined operator.

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum : forall n : nat, (ANum n) |\ n.

Error: Unknown interpretation for notation "_ |\ _".

My coq version is 8.4pl6(Nov. 2015). How can I make coq accept my new |\ operator?

Upvotes: 1

Views: 906

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

You need to append a where clause to the definition of your relation, as in the example in Software Foundations:

Reserved Notation "e |\ n" (at level 50, left associativity).

Inductive aexp := ANum : nat -> aexp.

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum : forall n : nat, (ANum n) |\ n

where "x |\ y" := (aevalR x y).

Upvotes: 3

Related Questions