The Coq mailing list

[Fabian Kunze <fkunze AT fakusb.de>]

Hi,

a workaround should be to manually specify one eta-expanded value to fail only once executed (and not during module initialisation):

Definition not_yet_implemented {A} : unit -> A. Admitted.
Extract Constant not_yet_implemented => "(fn x => failwith ""not yet implemented"")".  

usage:

Definition foo (x:nat) :bool := not_yet_implemented tt.

I hope this helps,

Fabian

Benjamin C. Pierce <bcpierce AT cis.upenn.edu> schrieb am Mo., 29. Mai 2017 um 16:21 Uhr:

I’d like to be able to extract an ML program from a Coq file that is missing some definitions.  For example, suppose I have a file temp.v containing

Definition foo (x:nat) : bool. Admitted.

Definition bar (x:nat) : bool := true.

and I want to play with bar before finishing foo.  If I do

Require Import temp.

Extraction Library temp.

what I get in temp.ml is

open Datatypes

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

let foo =

  failwith "AXIOM TO BE REALIZED"

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

let bar _ =

  Coq_true

which is not helpful (executing this code simply raises an error, whether or not foo is called).  

Is there a better way?

Thanks!

      - Benjamin