时间戳

首页 > 解决方案 > 在 Require Import coq 库之后混淆 bool 和 Datatypes.bool

coq - 在 Require Import coq 库之后混淆 bool 和 Datatypes.bool

问题描述

2

我正在研究软件基础并遇到错误。（https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html）

From Coq Require Import Arith.Arith.

From Coq Require Import Bool.Bool.

Require Export Coq.Strings.String.

From Coq Require Import Logic.FunctionalExtensionality.

From Coq Require Import Lists.List.

Import ListNotations.

证明示例：

Lemma eqb_stringP : forall x y : string,
    reflect (x = y) (eqb_string x y).

错误：在环境 x : string y : string 术语“eqb_string x y”的类型为“bool”，而预期的类型为“Datatypes.bool”。

关于如何进行的任何提示？

标签： coqlogical-foundations

解决方案

SF 在这里对 bool 有自己的定义：

https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html

尤其是在介绍性章节中，您需要小心不要将其与 Coq 的定义混淆。从 SF 导入文件或从标准库导入文件，但不能同时导入。

在后面的章节（公平）中，SF 切换到标准库定义。

推荐阅读