idris-0.9.11: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Delaborate

Documentation

bugaddr :: [Char]Source

delab :: IState -> Term -> PTermSource

delab' :: IState -> Term -> Bool -> Bool -> PTermSource

delabMV :: IState -> Term -> PTermSource

delabTy :: IState -> Name -> PTermSource

delabTy'Source

Arguments

:: IState 
-> [PArg]

implicit arguments to type, if any

-> Term 
-> Bool

use full names

-> Bool

Don't treat metavariables specially

-> PTerm 

pshow :: IState -> Err -> StringSource

pprintErr :: IState -> Err -> Doc OutputAnnotationSource