I was trying out coq extraction to haskell.
While extracting Coq's
nat to Haskell's
nat value like
2 gets extracted as
succ (succ 0) instead of just
succ (succ 0) matches the coq definition of
S (S O)).
Is there a way to make the extraction of
2:nat (Haskell) to be just
2:Integer (Haskell) instead of
succ (succ 0) (Haskell)?
(The same seems to happen in the ocaml extraction as well.)
This is what I had been trying:
Require Import ExtrHaskellBasic. Require Import ExtrHaskellNatInteger. Extraction Language Haskell. Definition foo := 2. Extraction foo. Recursive Extraction foo.
foo :: Prelude.Integer foo = Prelude.succ (Prelude.succ 0)
Can we make the
Prelude.succ (Prelude.succ 0) just
No. As you wrote, it matches the definition. So, it would require a lot of hardcoding in the extraction plugin to produce something else.
Could it make any difference if use a type other than
I would expect GHC’s optimizer to constant fold these expressions, maybe with some convincing
Last updated: Oct 04 2023 at 22:01 UTC