I'm trying to extract some programs from Coq into Haskell, have used the extraction libraries found here to map datatypes in Coq to the native datatypes in Haskell. My particular problem is with list (seq). The mapping works fine I have a declaration of
data Seq t = Nil | Cons t (Seq t) which then the rest of the functions on list within Haskell are defined on
Seq and not the native Haskell
(() a)polymorphic type for lists.
Is there anyway to stop
Seq from being extracted so the other Haskell functions on list will be defined correctly on the native Haskell lists?
have you looked at the coq-haskell project? For example, this has very detailed mappings to the Haskell stdlib: https://github.com/jwiegley/coq-haskell/blob/master/src/Haskell.v
Last updated: Jan 28 2023 at 06:30 UTC