如何解决Coq（Gallina语言，非Ltac）中列表自然数求和函数的“Syntax error: 'end' expected after [branches] (in [term_match])”语法错误？

我看到你遇到的问题了——同样是递归函数，自定义的add_left能正常运行，但是复制来的自然数列表求和函数却报了Syntax error: 'end' expected after [branches]的错误。这大概率是代码格式或者隐形符号导致的问题，下面给你分析原因和解决办法：

可能的原因 #

你的sum函数代码逻辑本身是正确的，但问题可能出在这两个地方：

• 单行分支的解析问题：Coq的解析器在处理单行写满所有match分支时，偶尔会出现识别错误，尤其是在jsCoq这类网页端环境中，对格式的敏感度更高。而你之前的add_left是分行排版的，解析器能清晰识别每个分支。
• 隐形特殊字符：如果是从其他地方复制的代码，可能混入了全角符号（比如中文的|、空格）或者不可见的控制字符，导致解析器无法正确识别分支结构。

解决办法 #

方法1：调整代码格式，分行书写分支 #

把match的每个分支单独换行并适当缩进，这是Coq社区的标准写法，既能避免解析错误，可读性也更强：

Fixpoint sum (l : list nat) : nat :=
  match l with
  | [] => 0
  | x :: xs => x + sum xs
  end.

方法2：检查并替换特殊字符 #

仔细检查代码中的所有符号：

• 确保|、::、+都是英文半角符号，没有混入全角字符
• 替换所有可能的全角空格为半角空格
• 如果怀疑有隐形字符，可以把代码复制到纯文本编辑器（比如Notepad++）中开启"显示所有字符"功能，排查并删除异常字符

验证测试 #

调整后你可以在本地Coq或jsCoq中测试这个函数，比如执行：

Compute sum [1;2;3].

应该能得到结果6，说明函数正常工作了。

内容的提问来源于stack exchange，提问作者Charlie Parker