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.

Answer 1

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.

Answer 2

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.