Idris.Core.Evaluate
normalise
normaliseTrace
normaliseC
normaliseAll
normaliseBlocking
toValue
quoteTerm
rt_simplify
simplify
specialise
hnf
convEq
convEq'
data Def
data CaseInfo
data CaseDefs
data Accessibility
type Injectivity
data Totality
data PReason
data MetaInformation
data Context
initContext
ctxtAlist
next_tvar
addToCtxt
setAccess
setInjective
setTotal
setMetaInformation
addCtxtDef
addTyDecl
addDatatype
addCasedef
simplifyCasedef
addOperator
lookupNames
lookupTyName
lookupTyNameExact
lookupTy
lookupTyExact
lookupP
lookupP_all
lookupDef
lookupNameDef
lookupDefExact
lookupDefAcc
lookupDefAccExact
lookupVal
mapDefCtxt
lookupTotal
lookupTotalExact
lookupInjectiveExact
lookupNameTotal
lookupMetaInformation
lookupTyEnv
isTCDict
isCanonical
isDConName
canBeDConName
isTConName
isConName
isFnName
data Value
class Quote a
initEval
uniqueNameCtxt
uniqueBindersCtxt
definitions
isUniverse