idris-0.10.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Delaborate

Synopsis

Documentation

annName :: Name -> Doc OutputAnnotation Source

bugaddr :: [Char] Source

delab :: IState -> Term -> PTerm Source

Delaborate a term without resugaring

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

-> Term 
-> Bool

use full names

-> Bool

Don't treat metavariables specially

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