idris-0.9.15: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Elab.Type

Synopsis

Documentation

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

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 TypeSource