coq - 错误消息：缺少的参数数量不正确（预期为 1）

Question

运行以下代码时遇到错误消息。

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]. 

我想知道我该如何解决它。谢谢。

Answer 1

你需要逗号：

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].