Zhangsheng Lai (Jun 06 2020 at 06:41): Zhangsheng Lai (Jun 06 2020 at 06:41):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?
Karl Palmskog (Jun 06 2020 at 12:11):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: Apr 19 2024 at 22:01 UTC