Idris.Delaborate

Documentation

annName :: Name -> Doc OutputAnnotation

bugaddr :: [Char]

delab :: IState -> Term -> PTerm

Delaborate a term without resugaring

delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm

delabDirect :: IState -> Term -> PTerm

Delaborate a term directly, leaving case applications as they are. We need this for interactive case splitting, where we need access to the underlying function in a delaborated form, to generate the right patterns

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

delabMV :: IState -> Term -> PTerm

delabSugared :: IState -> Term -> PTerm

Delaborate and resugar a term

delabTy :: IState -> Name -> PTerm

delabTy'

Arguments

:: IState

-> [PArg]

implicit arguments to type, if any

-> [(Name, Type)]

Names and types in environment (for properly hiding scoped implicits)

-> Term

-> Bool

use full names

-> Bool

Don't treat metavariables specially

-> Bool

resugar cases

-> PTerm

fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

Add extra metadata to an output annotation, optionally marking metavariables.

pprintDelab :: IState -> Term -> Doc OutputAnnotation

Pretty-print a core term using delaboration

pprintNoDelab :: IState -> Term -> Doc OutputAnnotation

pprintDelabTy :: IState -> Name -> Doc OutputAnnotation

Pretty-print the type of some name

pprintErr :: IState -> Err -> Doc OutputAnnotation

resugar :: IState -> PTerm -> PTerm

Re-add syntactic sugar in a term