[Agda] Does Agda compiler read haskell's type information?

Wolfgang Jeltsch wolfgang at cs.ioc.ee
Sun Apr 28 11:15:47 CEST 2013

Am Mittwoch, den 17.04.2013, 13:29 +0400 schrieb Станислав Черничкин:
> Hi, Agda dev team. 
> I'm interested in creating some tools which mind help with
> Agda-Haskell interoperation. In particular I interested in a tool for
> generating signatures in Agda for compiled Haskell functions and
> algebraic datatypes. For this purpose I need to extract type
> information from Haskell somehow, and generate Agda code.

I think you can use GHC as a library for this purpose:


Best wishes,

More information about the Agda mailing list