| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Elab.Type
Description
Synopsis
- buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris (Type, Type, PTerm, [(Int, Name)])
- elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type
- elabType' :: Bool -> ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type
- elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
- elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
Documentation
buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris (Type, Type, PTerm, [(Int, Name)]) Source #
Arguments
| :: ElabInfo | |
| -> SyntaxInfo | |
| -> Docstring (Either Err PTerm) | |
| -> [(Name, Docstring (Either Err PTerm))] | |
| -> FC | |
| -> FnOpts | |
| -> Name | |
| -> FC | The precise location of the name |
| -> PTerm | |
| -> Idris Type |
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 -> FC -> PTerm -> Idris Type Source #