Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Compiler.MAlonzo.HaskellTypes

Description

Translating Agda types to Haskell types. Used to ensure that imported Haskell functions have the right type.

# Documentation

haskellType :: QName -> HsCompileM Type Source #

checkConstructorCount :: QName -> [QName] -> [HaskellCode] -> TCM () Source #

hsTelApproximation :: Type -> HsCompileM ([Type], Type) Source #

hsTelApproximation' :: PolyApprox -> Type -> HsCompileM ([Type], Type) Source #