CODEWITHSUNDEEP
coq
Charlie Parker
Charlie Parker

Reputation: 5217

How does one divide two Nats in Coq?

I wanted to divide two numbers in Coq because I was trying to implement my own custom Imp language and had a statement:

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

however / returns an error:

Unknown interpretation for notation "_ / _".

and so does NDiv, error:

The reference NDiv was not found in the current environment.

what can I do so that I don't get this error?

How does one do something like the python "integer division" but with nats?

Upvotes: 2

Views: 1460

Answers (2)

Charlie Parker
Charlie Parker

Reputation: 5217

Seems like:

Require Import Coq.Init.Nat.

works, but I wonder how I could have searched this more efficiently without having to resort to put this trivial Q on SO.

Upvotes: 2

Li-yao Xia
Li-yao Xia

Reputation: 33519

You can use the command Require Import Arith. which will import, among other things, the function Nat.div and the notation _ / _ for it.

Upvotes: 4

Related Questions