Idris.Delaborate

Documentation

annName :: Name -> Doc OutputAnnotation

bugaddr :: [Char]

delab :: IState -> Term -> PTerm

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

delabMV :: IState -> Term -> PTerm

delabTy :: IState -> Name -> PTerm

delabTy'

Arguments

:: IState

-> [PArg]

implicit arguments to type, if any

-> Term

-> Bool

use full names

-> Bool

Don't treat metavariables specially

-> PTerm

fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

pprintDelab :: IState -> Term -> Doc OutputAnnotation

Pretty-print a core term using delaboration

pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

Pretty-print the type of some name

pprintErr :: IState -> Err -> Doc OutputAnnotation