Idris.Core.TT

data Option

data FC

fc_fname

fc_start

fc_end

spanFC

data FC'

emptyFC

fileFC

data NameOutput

data TextFormatting

data OutputAnnotation

data ErrorReportPart

data Provenance

data Err' t

type Err

data TC a

bindTC

score

tfail

failMsg

trun

discard

showSep

pmap

traceWhen

data Name

txt

str

tnull

thead

sUN

sNS

sMN

data SpecialName

sInstanceN

sParentN

showCG

type Ctxt a

emptyContext

mapCtxt

tcname

implicitable

nsroot

addDef

lookupCtxtName

lookupCtxt

lookupCtxtExact

deleteDefExact

updateDef

toAlist

addAlist

data NativeTy

data IntTy

intTyName

data ArithTy

nativeTyWidth

intTyWidth

data Const

isTypeConst

constIsType

constDocs

data Universe

data Raw

data ImplicitInfo

data Binder b

fmapMB

raw_apply

raw_unapply

data UExp

data UConstraint

data ConstraintFC

type UCs

data NameType

data AppStatus n

data TT n

class TermSize a

type EnvTT n

data Datatype n

data DataOpt

type DataOpts

data TypeInfo

A few handy operations on well typed terms:

isInjective

vinstances

instantiate

substV

explicitNames

pToV

pToV'

addBinder

pToVs

vToP

finalise

pEraseType

subst

psubst

substNames

substTerm

occurrences

noOccurrence

freeNames

arity

unApply

mkApp

unList

forget

safeForget

forgetEnv

safeForgetEnv

bindAll

bindTyArgs

getArgTys

getRetTy

uniqueNameFrom

uniqueName

uniqueNameSet

uniqueBinders

nextName

type Term

type Type

type Env

data WkEnvTT n

type WkEnv

itBitsName

showEnv

showEnvDbg

prettyEnv

showEnv'

pureTerm

weakenTm

weakenEnv

weakenTmEnv

orderPats

refsIn

liftPats

allTTNames

pprintTT

bindingOf