Как разделить два Натса в Coq?

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.

что я могу сделать, чтобы я не получил эту ошибку?

Как можно сделать что-то вродеPython "целочисленное деление", но с натс?

Answer 1

Похоже:

Require Import Coq.Init.Nat.

работает, но мне интересно, как я мог бы более эффективно искать это, не прибегая к установке этого тривиального Q на SO.

Answer 2

Вы можете использовать команду Require Import Arith., которая импортирует, среди прочего, функцию Nat.div и запись _ / _ для нее.