Error message: Not the right number of missing arguments (expected 1)

Question

I faced error message when running the following code.

Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1 ++ l2 <> l2 ++ l1.
Proof.
   exists bool [true] [false]. 

I'm wondering how I can solve it. Thanks.

Answer 1

You need commas:

Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1 ++ l2 <> l2 ++ l1.
Proof.
   exists bool, [true], [false].