The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

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?