时间戳

首页 > 解决方案 > 错误消息：缺少的参数数量不正确（预期为 1）

coq - 错误消息：缺少的参数数量不正确（预期为 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].

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

标签： coqcoqidecoq-extraction

解决方案

你需要逗号：

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

推荐阅读