Stream: Coq users

Topic: Extract only computed value

view this post on Zulip Julin Shaji (Oct 28 2023 at 15:59):

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: Oct 13 2024 at 01:02 UTC