The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hi List,

I wanted to represent arbitrary-precision integers in Coq, and
eventually also expect to extract them into OCaml's integers. My
questions are:
1) Can we use Z (http://coq.inria.fr/stdlib/Coq.ZArith.BinInt.html) to
present such arbitrary-precision integers in Coq? Z is defined
inductively. I think Coq extraction
(http://coq.inria.fr/refman/Reference-Manual027.html#toc139) only
allows to realize inductive Coq types into inductive OCaml types.  But
OCaml's int or big_bit is only primitive.

2) Coq.ZArith.Int defined an int, with comments :
(http://coq.inria.fr/stdlib/Coq.ZArith.Int.html)

"We define a signature for an integer datatype based on Z. The goal is
to allow a switch after extraction to ocaml's big_int or even int when
finiteness isn't a problem (typically : when mesuring the height of an
AVL tree). "

Do we have examples about how to use this int and extract it into OCaml?

Thanks in advance
-- 
Jianzhou