idris-1.3.0: Functional Programming Language with Dependent Types
Idris.ElabDecls
Description
Synopsis
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris () Source #
elabDecl' :: ElabWhat -> ElabInfo -> PDecl -> StateT IState (ExceptT Err IO) () Source #
elabDecls :: ElabInfo -> [PDecl] -> Idris () Source #
elabMain :: Idris Term Source #
Return the elaborated term which calls main
main
elabPrims :: Idris () Source #
Elaborate primitives
recinfo :: FC -> ElabInfo Source #
Top level elaborator info, supporting recursive elaboration