在 Coq 中，如何从命名空间中删除定义的变量？

Question

在coqtop交互式终端中，如何删除我定义的名称？

例如，我可以定义一个 bool 类型，如下所示。

Coq < Inductive my_bool : Type :=
Coq < | my_true : my_bool
Coq < | my_false : my_bool.

这有效，我得到以下输出。

my_bool is defined
my_bool_rect is defined
my_bool_ind is defined
my_bool_rec is defined

但是，如果我想重新定义 my_bool 项，我会得到 Error: my_bool already exists.

> Inductive my_bool : Type :=
> | my_true : my_bool
> | my_false : my_bool
> | neither : my_bool.
Error: my_bool already exists.

我可以在不退出 coqtop 会话的情况下删除并重新定义 my_bool 术语吗？

Answer 1

您可以使用 Reset my_bool. 将其从环境中删除。

参考：https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.reset：

Reset ident removes all the objects in the environment since ident was introduced, including ident. ident may be the name of a defined or declared object as well as the name of a section. One cannot reset over the name of a module or of an object inside a module.

在 Coq 中，如何从命名空间中删除定义的变量？

In Coq, how to remove a defined variable from the namespace?

coq