idris-0.12.3: Functional Programming Language with Dependent Types
Idris.ElabDecls
Description
Synopsis
recinfo :: FC -> ElabInfo Source #
Top level elaborator info, supporting recursive elaboration
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 -> StateT IState (ExceptT Err IO) () Source #