How to solve the very simple Syntax error: 'end' expected after [branches] (in [term_match]). in Coq? (in Gallina and not ltac)

Question

I was trying to write a very simple program to sum nats in a list (copy pasted from here):

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

but my local Coq and jsCoq complain:

Syntax error: 'end' expected after [branches] (in [term_match]).

Why is this? (note I didn't even implement this but my implementation looks the same pretty much)

I've implemented recursive functions before:

  Inductive my_nat : Type :=
    | O : my_nat
    | S : my_nat -> my_nat.

  Fixpoint add_left (n m : my_nat) : my_nat := 
    match n with
    | O => m
    | S n' => S (add_left n' m)
  end.

which doesn't complain...

I did see this question How to match a "match" expression? but it seems to address some special issue in ltac and I am not using ltac.

score 3 · Accepted Answer · answered Mar 19 '22 at 15:04

3

The location of the error is on the [], which suggests that Coq does not understand that notation. Upon finding undefined notation, the parser has no idea what to do and produces an essentially meaningless error message.

To have standard list notation be defined, you need to import it from the standard library via:

Require Import List.
Import ListNotations.

The stdlib module List contains the module ListNotations, which defines [] (and more generally [ x ; y ; .. ; z ]). List also defines the notation x :: xs.

answered Mar 19 '22 at 15:04

mudri

758
3
16

1

The fact that syntax actually depends on which modules you have loaded is unfortunate. It never came to my mind before that it could be so frustrating to people wishing to learn the language. – Yves Mar 19 '22 at 16:47
@Yves well hopefully that will be less hard now that they can google the error (when my error happened nothing in google was useful). But this question and answer hopefully will change that :) – Charlie Parker Mar 21 '22 at 12:45
I just added a answer of my own, but I think it would be better if something similar was included in the answer by @mudri. – Yves Mar 22 '22 at 07:27

score 0 · Answer 2 · answered Mar 22 '22 at 07:25

when picking up excerpts from a development, you also have to find what are the syntax changing commands that have an effect on this exceprts: Module importation, scope opening, argument declarations (for implicits), Notations, and coercions". In the current case, the file is actually provided by the author of the exercises through this pointer.

How to solve the very simple Syntax error: 'end' expected after [branches] (in [term_match]). in Coq? (in Gallina and not ltac)

2 Answers2