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.