coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Redefinition of extracted parameter

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Redefinition of extracted parameter
Date: Fri, 21 Sep 2018 17:16:54 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay7-d.mail.gandi.net
Ironport-phdr: 9a23:nGf1mRwVveeznObXCy+O+j09IxM/srCxBDY+r6Qd1OIUIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH1likHOT43/mLZhMN+g61Uog6uqRNkzo7IY4yYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YBDvAOOvpEr4bnoVsBtRqwBQioBOz01DBInGP21rA93uQuCw7JwhAgEMgIsHjOo9X1NaMSXvurw6nS0TXOdOhW2TT96YjTcRAhoPSMXbdufsrL00UvER3KjkmJpIHjIjib1fwNvnCF4+Z9V++jkWwqpx1rrjSyxcohhJPFipwJxlzY7Sl0wZg5KcelREJnf9KoCoZcui6ZOodsX88vQGNltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wr5VOmPJTd3nnJkdbCmixmv60Sgz/fzVsiw0FpQoSpKiN/MuW0M1xDJ7MiIVOd98l+g2TaJyQ/T9vlJLV4pmafZMZIswKI8moAOvUnAECL6glv6gLOKekk8/+in8eXnYrHopp+GMI90jxnzMqs0lcOhHeQ3KA4OU3KU+eS90L3s5lP2QK9WjvAtianZs5DbJd8Ypq64Bg9V15gs6wylAzegztsYgWELLEhZdxKfk4jpJ1bOLejkAve4mlSgiStkx/TbPrL6GZjNNXjCkLL5fbln8UJcyQwzzcpe551OEL0BLujzCQfNs4nTCQZ8OAipyc7mDs9838UQQzGhGKicZYzbMkOB4NUAIu2GaZUJ8GLyIvU57viogn49k1IHYYGy3ooMa3G9G/l8ZUOUfSy/0Z86DW4Ws19mH6TRg1qYXGsLPifgb+cH/jg+TbmeI8LGT4GpjqaG2X7lTIZVd3tFC1WJHG2ucYiYCa5VNHCiZ/R5mzlBboCPDpc73Ejw5hT52qFkL+/R9zdes5//hoAsur/j0Coq/DkxNPyzlmGAS2YuwzESSjs/zf86rQp4w1aHl6dxhfBZU9pe+6ERXw==

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

Gaëtan Gilbert

On 21/09/2018 16:44, King, Oscar wrote:

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

[Coq-Club] Redefinition of extracted parameter, King, Oscar, 09/21/2018
- Re: [Coq-Club] Redefinition of extracted parameter, Gaëtan Gilbert, 09/21/2018
- <Possible follow-up(s)>
- Re: [Coq-Club] Redefinition of extracted parameter, King, Oscar, 09/26/2018
  - Re: [Coq-Club] Redefinition of extracted parameter, Maximilian Wuttke, 09/27/2018