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

Question

So I have this code:

Require Import Unicode.Utf8.
Require Import String.

Inductive AExp :=
| avar : string → AExp 
| anum : nat → AExp 
| aplus : AExp → AExp → AExp 
| amul : AExp → AExp → AExp.

Coercion anum : nat >-> AExp.
Coercion avar : string >-> AExp.
Notation "A +' B" := (aplus A B) (at level 50, left associativity).
Notation "A *' B" := (amul A B) (at level 40, left associativity).

Inductive BExp :=
| btrue : BExp
| bfalse : BExp
| bnot : BExp → BExp
| band : BExp → BExp → BExp
| blessthan : AExp → AExp → BExp
| bgreaterthan : AExp → AExp → BExp.

Notation "A <' B" := (blessthan A B) (at level 80).
Notation "A >' B" := (bgreaterthan A B) (at level 80).
Infix "and'" := band (at level 82).
Notation "! A" := (bnot A) (at level 81).

Inductive Stmt :=
| assignment : string → AExp → Stmt 
| while : BExp → list Stmt → Stmt
| seq : Stmt → Stmt → Stmt
| obj_inst : string → string → Stmt
| method_invoke : string → string → list AExp → Stmt.

Notation "X ::= A" := (assignment X A) (at level 85).
Notation "S1 ;; S2" := (seq S1 S2) (at level 99, right associativity).

Inductive Method :=
| method : string → list Stmt → Method.

Inductive Class :=
| class : string → list (string * AExp) → list Method → Class.

Definition Point :=
  class "Point"
    [("x", anum 0) ("y", anum 0)]
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

Definition CreatePoint : Stmt :=
  obj_inst "p" "Point".

Definition MovePoint : Stmt :=
  method_invoke "p" "move" [].

Definition SampleProgram :=
  seq CreatePoint MovePoint.

and I got this error:

Syntax error: '.' expected after [gallina] (in [vernac_aux]). And I am not sure if it's because of the Definition Point.

Tried using chatGpt and it didn't work. Using it I wasted a lot of time. (i don't know what to write mroe so StackOverflow would let me post this question)

Answer 1

(Looks like some old Coq code that needs some freshening up.)

Typically, you cannot use notations without importing/opening them: and your code is missing both list and string notations.

Here is the fix for that, as well as a fix to the StdLib imports, as with your code you could have name conflicts/ambiguities:

From Coq Require Import Unicode.Utf8.
From Coq Require Import String.
From Coq Require Import List.

Import ListNotations.
Open Scope string.

...etc...

I have had also to fix a missing semicolon here:

Definition Point :=
  class "Point"
    [("x", anum 0); ("y", anum 0)]  (* <- semicolon in list *)
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

Now it compiles...