coq - 在 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.

我可以删除并重新定义 my_bool术语而不退出 coqtop session ？

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.