Blagda.Agda

Documentation

moduleName :: FilePath -> String

fakePath :: QName -> Maybe FilePath

removeImpls :: Expr -> Expr

runAgda :: (String -> TCMT IO a) -> IO a

setupTCM :: TCMT IO String

killDomainNames :: Type -> Type

killQual :: Expr -> Expr

tcAndLoadPublicNames :: FilePath -> String -> TCMT IO (Map Text Text)

makePi :: [TypedBinding] -> Expr -> Expr

builtinModules :: [String]