idris-0.9.20: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Type

Synopsis

Documentation

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".