在 Coq 中如何划分两个 Nat？

Question

我想在 Coq 中将两个数字相除，因为我试图实现自己的自定义 Imp 语言并有一个声明：

    match (aeval st a1) with
      | Some n0 => Some (NDiv n0 (S n))
      | None => None

然而/ 返回错误：

Unknown interpretation for notation "_ / _".

NDiv 也是，错误：

The reference NDiv was not found in the current environment.

我该怎么做才能不出现此错误？

如何使用 nats 来执行类似于 python“整数除法”的操作？

Answer 1

您可以使用命令Require Import Arith.，其中将导入函数Nat.div 和符号_ / _。

Answer 2

好像：

Require Import Coq.Init.Nat.

有效，但我想知道如何才能更有效地搜索它，而不必求助于将这个微不足道的 Q 放在 SO 上。