Hello everybody,
I have a file Sample.v with the content
Require Import String.
Require Import Int63.Sint63.
Require Import PArray.
Require Import Ascii String Coq.Strings.Byte.
Module Sample.
Definition bytes : Set := string.
Definition len_bytes (s:bytes) := 1+ length s.
End Sample.
and a file with the content
Require Export Sample.
Require Extraction.
Require ExtrOcamlBasic.
Require ExtrOCamlInt63.
Require ExtrOcamlChar.
Require ExtrOcamlNativeString.
Extraction Language OCaml.
Extraction Library Sample.
When I extract the Ocaml code I get
open Datatypes
open Nat
open String
module Sample =
struct
type bytes = string
(** val to_bytes : string → nat **)
let len_bytes s =
add (S O) (length s)
end
And now my question comes. Where I can find the compiled code/library/interfaces
for the modules Nat, Datatypes and String?
Of course I can extract them and compile myself, but this triggers generation of
other modules. This is actually good enough, but maybe there is some simpler
way to compile my extracted sample (precompiled libraries or something). I have
already spent a good deal of time looking for a solution, but I did not find one.
All the best,
Alx