Idris.ElabTerm
data ElabMode
build
buildTC
getUnmatchable
data ElabCtxt
initElabCtxt
goal_polymorphic
elab
pruneAlt
pruneByType
findInstances
solveAuto
solveAutos
trivial'
proofSearch'
resolveTC
resTC'
collectDeferred
case_
runTac
reflm
reify
reifyApp
reifyTT
reifyTTApp
reifyRaw
reifyRawApp
reifyTTName
reifyTTNameApp
reifyTTNamespace
reifyTTNameType
reifyTTBinder
reifyTTBinderApp
reifyTTConst
reifyTTConstApp
reifyArithTy
reifyNativeTy
reifyIntTy
reifyTTUExp
reflCall
reflect
claimTT
reflectQuotePattern
reflectQuote
reflectNameType
reflectName
reflectNameQuotePattern
reflectBinder
reflectBinderQuote
mkList
reflectConstant
reflectUExp
reflectEnv
rawBool
rawNil
rawCons
rawList
rawPairTy
rawPair
reflectCtxt
reflectErr
elaboratingArgErr
withErrorReflection
fromTTMaybe
reflErrName
reifyReportPart
envTupleType
solveAll