idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Delaborate

Synopsis

Documentation

delabTy' Source

Arguments

:: IState 
-> [PArg]

implicit arguments to type, if any

-> Term 
-> Bool

use full names

-> Bool

Don't treat metavariables specially

-> PTerm 

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

Pretty-print a core term using delaboration

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

Pretty-print the type of some name