idris-0.9.20: Functional Programming Language with Dependent Types
Idris.ElabDecls
Synopsis
recinfo :: ElabInfo Source
elabMain :: Idris Term Source
Return the elaborated term which calls main
main
elabPrims :: Idris () Source
Elaborate primitives
elabDecls :: ElabInfo -> [PDecl] -> Idris () Source
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris () Source
elabDecl' :: ElabWhat -> ElabInfo -> PDecl' PTerm -> StateT IState (ExceptT Err IO) () Source