bool和Datatypes.Pool在需要导入coq库之后的混合

Question

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 xy"；具有类型"；bool"；而预期其具有类型"0"；数据类型.bool"；。

有关于如何继续的提示吗？

Answer 1

SF在这里有自己的布尔定义：

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

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

在后面的章节(afair(中，SF切换到标准库定义。