Deriving instances for Haskell extracted data-types

Using Coq
1

I am extracting to Haskell which is very exciting:

data Coq_signal =
   Bit
 | Tuple2 Coq_signal Coq_signal

Is it possible to extract a datatype declaration which has some deriving instances for things like Show and Eq e.g. to produce something like:

data Coq_signal =
   Bit
 | Tuple2 Coq_signal Coq_signal
 deriving (Eq, Show)

Thank you!

2

My solution to this issue when it has popped up is to just use the -XStandaloneDeriving language extension in Haskell. See: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#stand-alone-deriving-declarations

1 Like
3

Yes, thank you. That is what I was going to do otherwise and I guess it seems like a plausible solution.

4

Enrico Tassi made a Deriving extension using Elpi in Coq.
https://hal.inria.fr/hal-01897468v2/document

1 Like