所以我有这个代码：
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.
我得到了这个错误：
语法错误：[gallina] 后应为“.”（在 [vernac_aux] 中）。我不确定是否是因为
Definition Point.
尝试使用 chatGpt，但没有用。使用它我浪费了很多时间。（我不知道该写些什么，这样 StackOverflow 才会允许我发布这个问题）