coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Redefinition of extracted parameter

From: "King, Oscar" <oscar.king.16 AT ucl.ac.uk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Redefinition of extracted parameter
Date: Fri, 21 Sep 2018 14:44:59 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oscar.king.16 AT ucl.ac.uk; spf=None smtp.mailfrom=oscar.king.16 AT ucl.ac.uk; spf=Pass smtp.helo=postmaster AT EUR01-DB5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:HIOmuBEdNDQDSpvsb1h9H51GYnF86YWxBRYc798ds5kLTJ7zos2wAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoBO9qBNw2IPbep2ZNP9kc6/BYd8XR2xMVdtRWSxbBYO8apMCA+QEM+ZZqYn9qEMCpganCwm3GOzg0CVIinHr1qA91OQhCh3J0xY6H94Us3TUrdP1NKgIXeyozaTF1ijDYO9S2Tvn8ofHbgotoeyPXb9pd8fa1EohFxvdg1mNtYDoMCmZ2+sPvmSB8eZsT/+jh3Mmpg1pvzSiycghhpPKi44L0FzJ9j91zJs2KNC4UEJ7b8CrHZhMuyyfMoZ7QsAvTmB2tys/xbALuYC0cScPxZkmxhPQcOeIfo2K7x/tSumeOjF1j29/dr2lnRa9602gx/X8Vsaq1FZKqTJInNbCuX4RyxDf99GLRPVg80qhwDqP0Bvc5f9eLUAziKrbN4UuwrktlpoVrEvPBDf2mF/xjK+KaEor5vSo6+XgYrXgvJOcMJJ0ih36MqQpncy/Av40PRQJX2ie4ei81bvj8lPlQLhSk/E6jqbUvIrVKMkZvKK1HRVZ3ps+5xu+Fzum1c4XnXgDLFJLYhKHiI3pNknJIPDjEfiwmU6snC1ox/DHOL3hDY/BImXCnbr6YLZy90pcxBApwt9D/Z5UF7IBLOrpWkDtrNzYEgM5Mwuszun7D9V9z5oSVn6LAq+EK6zfqkSI5+IqI+mUfoAZojf9K/4/5/7vl3A1g1EdfbP6lacQPTqzGe0jKEGEa1LthM0AGCEEpEB2GOftkRiJVSNZT3e0RaM1oD8hXtGIF4DGE8qOgbqOmG+cBZZffCoOXleXGn7yMYaFXfhKMXy6P8Rl1DUPE6WiHdxynSqyvRP3nuI0ZtHf/TcV4Mq6hYpFotbLnBR3zgRaSsGU0mWDVWZxxzpaWjQymql051F+mA/ajfpIxsdAHNkW3MtnFx8gPMeFnfFxD5b7UUTcfYXREQv0cpCdGTg0C+kJ7ZoObkJ6R4rwoy35h3PvL5VI0ruBCdoz777W2GX3K4Bl0XHa2aI9jl4gBMxSKWmhga05/A/WVdfE
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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