The Coq mailing list

[Wouter Swierstra <w.swierstra AT cs.ru.nl>]

Hi Trevor, cc-Pierre,

> Is this a limitation of the extraction plugin, or am I missing
> something when extracting Haskell?

Using the following commands produces pretty much what I'd expect to see:

> Extraction Language Haskell.
> Extract Inductive Datatypes.nat => "Integer" ["0" "succ"]
>   "(\fO fS n -> if n==0 then fO () else fS (n-1))".
> Extract Inlined Constant plus => "(+)".
> Extract Inlined Constant mult => "(*)".
> Extraction fact_body.
> Extraction fact.

But using "Recursive Extraction fact" seems to generate too much code:
it also produces code for mult and plus, which is exactly what the
Extract Inlined Constant commands should avoid... Is that the same
behaviour you're seeing?

All the best,

  Wouter