coq - 在 Coq 中如何将两个 Nats 相除？

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和符号 _ / _为了它。