idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Type

Synopsis

Documentation

buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris (Type, Type, PTerm, [(Int, Name)]) Source

elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> PTerm -> Idris Type Source

Elaborate a top-level type declaration - for example, "foo : Int -> Int".

elabType' :: Bool -> ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> PTerm -> Idris Type Source

elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> FnOpts -> Name -> PTerm -> Idris () Source