idris-0.9.12: Functional Programming Language with Dependent Types

Safe HaskellNone

IRTS.Compiler

Documentation

compile :: Codegen -> FilePath -> Term -> Idris ()Source

irMain :: TT Name -> Idris LDeclSource

mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]Source

showCaseTrees :: [(Name, LDecl)] -> StringSource

isCon :: Def -> BoolSource

class ToIR a whereSource

Methods

ir :: a -> Idris LExpSource

Instances

ToIR SC 
ToIR (TT Name) 
ToIR ([Name], SC) 

build :: (Name, Def) -> Idris (Name, LDecl)Source

getPrim :: IState -> Name -> [LExp] -> Maybe LExpSource

declArgs :: [Name] -> Bool -> Name -> LExp -> LDeclSource

mkLDecl :: Name -> Def -> StateT IState (ErrorT Err IO) LDeclSource

getFTypes :: TT Name -> Maybe [FType]Source

mkIty' :: TT Name -> FTypeSource

mkIty :: [Char] -> FTypeSource

mkIntIty :: [Char] -> FTypeSource

zname :: NameSource

sname :: NameSource