Skip to content

Pretty printing data type declarations

It might be a good idea to print the type of both the data type and its constructor. Imagine we have:

data Blah a where
  MkBlah1 :: Int -> Blah Int
  MkBlah2 :: String -> Blah String

Then we should print it as something like:

type Blah : Type -> Type
constructors:
  MkBlah1 : Int -> Blah Int
  MkBlah2 : String -> Blah String

We could also print:

Blah : Type -> Type
MkBlah1 : Int -> Blah Int
MkBlah2 : String -> Blah String
Edited by Artin Ghasivand