I have a file `term.v`

that looks like this:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(* Grammer of a term *)
Inductive Term : Type :=
(* bounded variable with binder removed,identified using debruijn-levels *)
| var (idx: nat): Term
(* Universes.. TODO this must be replaced with subtyping based universes *)
| univ (l: nat): Term
(* Function type from A to B*)
| pi (A: Term) (B: Term)
(* Lambda Abstraction (Function implementation) *)
| lam (T: Term) (y: Term)
(* Function Application *)
| appl (m: Term) (n: Term)
(* sigma type*)
| sigma (A: Term) (B: Term)
(* dependent pairs*)
| pair (M N: Term) (m: Term) (n: Term)
(* projection for dependent pair *)
| proj1 (m: Term)
| proj2 (m: Term).
Tactic Notation "TermElim" :=
elim => /=
[ idx
| lvl
| A IHA B IHB
| T IHT y IHy
| m IHm n IHn
| A IHA B IHB
| M IHM N IHN m IHm n IHn
| m IHm
| m IHm
].
```

In a different file, Ido the following to extract

```
From Coq Require Extraction.
From Coq Require Import ExtrOcamlBasic ExtrOcamlNatBigInt.
Set Warnings "-extraction-opaque-accessed".
Cd "src".
Separate Extraction term.
```

I get the expected `term.ml `

`term.mli`

but there also two strange empty files called `Datatypes.ml`

` Datatypes.mli`

. How to get rid of them ?

one more thing in term.ml, I see inductive principles being extracted, and I don't think I will ever need them, how to prevent those from being extracted ?

datatypes is used for nat, but ExtrOcamlNatBigInt replaces the inductive nat so it ends up empty

walker said:

one more thing in term.ml, I see inductive principles being extracted, and I don't think I will ever need them, how to prevent those from being extracted ?

you can unset https://coq.github.io/doc/master/refman/proofs/writing-proofs/reasoning-inductives.html#coq:flag.Elimination-Schemes when declaring the inductive if you really don't need them

Gaëtan Gilbert said:

datatypes is used for nat, but ExtrOcamlNatBigInt replaces the inductive nat so it ends up empty

but is there a way to not have the file ?

now that we are at it, extracting some other file gives a strange warning

```
The identifier Datatypes_nat__canonical__eqtype_Equality contains __ which is
reserved for the extraction [extraction-reserved-identifier,extraction]coqtop
```

Is that something I need to be concerned about ?

I am getting a strange error typing to compile the extracted code:

```
1046 | ......let h0 = h fix_0 in
1047 | (fun _UU0393_ t3 fuel ->
1048 | let (a, b) = h0 in
1049 | let (a0, b0) = b in
1050 | let (a1, b1) = b0 in
...
1083 | (a1 _UU0393_ m fuel))
1084 | | Coq_proj2 m ->
1085 | Coq_type_infer_graph_equation_9 (_UU0393_, m, fuel,
1086 | (a1 _UU0393_ m fuel))))
Error: This kind of expression is not allowed as right-hand side of `let rec`
```

Last updated: Jun 16 2024 at 03:41 UTC