For extraction, is it possible to do the computation first and then extract out only the result of the computation?

```
Require Import Extraction.
Definition incr (n: nat): nat := S n.
Fixpoint addn (n m: nat): nat :=
match n with
| O => m
| S n' => S (addn n' m)
end.
Example result2 := addn 2 3.
Extraction Inline addn.
Recursive Extraction result2.
```

This gave:

```
type nat =
| O
| S of nat
(** val result2 : nat **)
let result2 =
let rec addn n m =
match n with
| O -> m
| S n' -> S (addn n' m)
in addn (S (S O)) (S (S (S O)))
```

Is it possible to have the `match`

reduced as well in the extracted code?

To get only the value, without having to keep the definition of `addn`

?

So that it would become `nat`

value for 5.

`Extraction Inline`

apparently couldn't do that.

Last updated: Jun 22 2024 at 15:01 UTC