How to properly load type Int from Coq.ZArith.Int?

Question

I'm new to coq and I am trying to use the "int" type from ZArith.Int but coq cannot find it.

Require Export ZArith Int.
Open Scope Int_scope.

when I use "int" in my definitions such as (... -> int -> ...), coq cannot find it. How can I properly load it along with the library's operations?

Answer 1

That library actually formalizes an abstract module of integers, that can be later instantiated with a concrete implementation. In Coq, the implementation of integers from the standard library is called Z. There's an instance of the Int module type in terms of Z defined in that library, called Z_as_Int; to use the definitions available there with Z, you just need to refer to them prefixed by the module name, e.g. Z_as_Int._0. However, given that most theorems are proven directly over Z, without relying on the interface defined in Int, it is probably better to just use Z directly.