idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Elab.Type

Description

 

Synopsis

Documentation

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

elabType 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 #

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

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