License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Delaborate

Description

Synopsis

Documentation

annName :: Name -> Doc OutputAnnotation Source #

bugaddr :: [Char] Source #

delab :: IState -> Term -> PTerm Source #

Delaborate a term without resugaring

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

delabDirect :: IState -> Term -> PTerm Source #

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 Source #

delabMV :: IState -> Term -> PTerm Source #

delabSugared :: IState -> Term -> PTerm Source #

Delaborate and resugar a term

delabTy :: IState -> Name -> PTerm Source #

delabTy' Source #

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 Source #

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

pprintDelab :: IState -> Term -> Doc OutputAnnotation Source #

Pretty-print a core term using delaboration

pprintNoDelab :: IState -> Term -> Doc OutputAnnotation Source #

pprintDelabTy :: IState -> Name -> Doc OutputAnnotation Source #

Pretty-print the type of some name

pprintErr :: IState -> Err -> Doc OutputAnnotation Source #

resugar :: IState -> PTerm -> PTerm Source #

Re-add syntactic sugar in a term