idris-0.9.15: Functional Programming Language with Dependent Types
Idris.ElabDecls
Synopsis
recinfo :: ElabInfoSource
elabMain :: Idris TermSource
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 (ErrorT Err IO) ()Source