The Coq mailing list

[t x <txrev319 AT gmail.com>]

Worked. Thanks!

On Mon, Sep 2, 2013 at 6:24 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:

Hi,

You need to import the list notations:

Require Import List.
Import ListNotations.

Eval compute in [1; 2].

On Mon, Sep 2, 2013 at 8:20 AM, t x <txrev319 AT gmail.com> wrote:
> Hi,
>
>   I'm trying to use Coq's List Notation of [ .. ; .. ; .. ].
>
>   I try the following:
>
> Require Import List.
> Local Open Scope list_scope.
>
> Eval compute in [1; 2].
>
>
>   Instead of getting a (1 :: 2 :: nil), I get back
>
>   Syntax error: [constr: lconstr] expected after 'in' ...
>
> What am I doing wrong?