27 lines
683 B
Coq
27 lines
683 B
Coq
Require Extraction.
|
|
Extraction Language Haskell.
|
|
Require Import ExtrHaskellBasic.
|
|
Require Import ExtrHaskellString.
|
|
|
|
Require Import ExtrHaskellNatInt.
|
|
Require Import ExtrHaskellZInt.
|
|
|
|
(*
|
|
Require Import ExtrHaskellNatInteger.
|
|
Require Import ExtrHaskellZInteger.
|
|
Require Import ExtrHaskellNatNum.
|
|
Require Import ExtrHaskellZNum.
|
|
*)
|
|
|
|
Set Extraction File Comment "Made from Coq".
|
|
Extract Inlined Constant fst => "Prelude.fst".
|
|
Extract Inlined Constant snd => "Prelude.snd".
|
|
Extraction Blacklist Main.
|
|
|
|
|
|
Definition mac' (acc: nat) (xy: nat*nat): nat := acc + ((fst xy)*(snd xy)).
|
|
|
|
Definition topFn (acc: nat) (xy: nat*nat) : nat * nat := (mac' acc xy, acc).
|
|
|
|
Recursive Extraction topFn.
|