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