# How does one import native cyclic integers in coq?
**URL:** https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003
**Category:** Using Rocq
**Created:** [August 1, 2023, 8:40am UTC](https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003 "2023-08-01T08:40:56Z")
**Posts on this page:** 4
**Page:** 1
### Author:  [@randl](https://discourse.rocq-prover.org/u/randl)
#### Post date: [August 1, 2023, 8:40am UTC](https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003/1 "2023-08-01T08:40:56Z")
Hi,
I’m looking to work with native OCaml integers in Coq, with the objective of extracting the program and running it natively.
My problem is that I can’t seem to understand what “Require Import” command to use to import these integers. My understanding is that they are stored in stdlib (as suggested by [Standard Library | The Coq Proof Assistant](https://coq.inria.fr/stdlib/)) but all of my attempts (Require Import Numbers, Require Import Int63, etc) have given me the following **Error:** `Cannot find a physical path bound to logical path`.
Any hints would be very appreciated.
Best,
MRandl
---
### Author:  [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)
#### Post date: [August 1, 2023, 11:05am UTC](https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003/2 "2023-08-01T11:05:06Z")
If you look at the page e.g. for Uint63:
[https://coq.inria.fr/stdlib/Coq.Numbers.Cyclic.Int63.Uint63.html](https://coq.inria.fr/stdlib/Coq.Numbers.Cyclic.Int63.Uint63.html)
you’ll see at the vey top “Library Coq.Numbers.Cyclic.Int63.Uint63”.
That given, in your code you could simply write:
`Require Coq.Numbers.Cyclic.Int63.Uint63.`
The point is those are _logical paths_ and Coq needs to be told how those map to _physical paths_ on disk. The code above works if you start coqc/coqtop with default options, otherwise there are command line options or the use of `_CoqProject` files to do that/your mapping (e.g. custom defined paths in \_CoqProject files is common to share code among one’s projects).
See the docs for more details, e.g. here: [https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=\_coqproject#logical-paths-and-the-load-path](https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=_coqproject#logical-paths-and-the-load-path) and here: [https://coq.inria.fr/refman/practical-tools/coq-commands.html#command-line-options](https://coq.inria.fr/refman/practical-tools/coq-commands.html#command-line-options)
---
### Author:  [@randl](https://discourse.rocq-prover.org/u/randl)
#### Post date: [August 1, 2023, 11:39am UTC](https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003/3 "2023-08-01T11:39:04Z")
I see. Thanks a lot, that was very instructive!
MRandl
---
### Author:  [@jfehrle](https://discourse.rocq-prover.org/u/jfehrle)
#### Post date: [August 2, 2023, 5:44pm UTC](https://discourse.rocq-prover.org/t/how-does-one-import-native-cyclic-integers-in-coq/2003/4 "2023-08-02T17:44:22Z")
**From Coq Require Uint63.** is sufficient provided that there is only one package matching **Coq. … .Uint63**
**From** is not required, but it avoids name clashes if you later load another package that defines its own **Uint63**.
See [https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Require](https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Require)