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

Nils Anders Danielsson nad at chalmers.se
Wed Apr 17 11:37:46 CEST 2013


On 2013-04-17 11:29, Станислав Черничкин wrote:
> And I wondering, probably Agda compiler is already able to extract
> type information from Haskell somehow?

No. (Except that generated code is type-checked by GHC, so Agda gets
information about whether GHC accepts the code or not.)

-- 
/NAD



More information about the Agda mailing list