[Coq-Club] Redefinition of extracted parameter

[King, Oscar]

Hi,

I’m trying to extract some code with parameters that I want to define in OCaml however when I extract and try to redefine by defining function or type with the same name I get type conflicts between files. I have constructed an example below:

How would I redefine foo in the extracted code properly?

Thanks in advance,

Oscar

Parameter foo: nat -> nat -> nat.

Definition bar x := foo x.

Require Extraction.

Recursive Extraction bar.

(* Extracted Code *)
type nat =
| O
| S of nat

(** val foo : nat -> nat -> nat **)

let foo =
failwith "AXIOM TO BE REALIZED"

(** val bar : nat -> nat -> nat **)

let bar =
foo

[Gaëtan Gilbert]

I'm only seeing one file and no type conflict.

Gaëtan Gilbert

Hi,
I’m trying to extract some code with parameters that I want to define in
OCaml however when I extract and try to redefine by defining function or
type with the same name I get type conflicts between files. I have
How would I redefine foo in the extracted code properly?
Thanks in advance,
Oscar
Parameter foo: nat -> nat -> nat.
Definition bar x := foo x.
Require Extraction.
Recursive Extraction bar.
(* Extracted Code *)
type nat =
| O
| S of nat
(** val foo : nat -> nat -> nat **)
let foo =
  failwith "AXIOM TO BE REALIZED"
(** val bar : nat -> nat -> nat **)
let bar =
  foo