Idris.Core.Evaluate

normalise

normaliseTrace

normaliseC

normaliseAll

rt_simplify

simplify

specialise

hnf

convEq

convEq'

data Def

data CaseInfo

data CaseDefs

data Accessibility

data Totality

data PReason

data MetaInformation

data Context

initContext

ctxtAlist

uconstraints

next_tvar

addToCtxt

setAccess

setTotal

setMetaInformation

addCtxtDef

addTyDecl

addDatatype

addCasedef

simplifyCasedef

addOperator

lookupNames

lookupTyName

lookupTyNameExact

lookupTy

lookupTyExact

lookupP

lookupDef

lookupNameDef

lookupDefExact

lookupDefAcc

lookupDefAccExact

lookupVal

mapDefCtxt

lookupTotal

lookupNameTotal

lookupMetaInformation

lookupTyEnv

isTCDict

isDConName

isTConName

isConName

isFnName

data Value

class Quote a

initEval

uniqueNameCtxt

uniqueBindersCtxt

definitions

isUniverse