inductive Hex.RCF.HandlerResult : Type

An optional handler either declines the source syntax, reports a terminal failure (including false verdicts and exhausted/rejected replay), or proposes an ordinary proof of the original goal.

• declined : HandlerResult

  This handler does not recognize the source syntax.

• failed (message : Lean.MessageData) : HandlerResult

  Recognized syntax failed; no subsequent handler may run.

• proved (proof : Lean.Expr) : HandlerResult

  A candidate proof, checked by the base before goal assignment.

@[reducible, inline]

abbrev Hex.RCF.Handler : Type

Optional coefficient solvers receive the unchanged source target.

Equations

• Hex.RCF.Handler = (Lean.Expr → Lean.MetaM Hex.RCF.HandlerResult)

def Hex.RCF.handlerNames : Lean.CoreM (Array Lean.Name)

Registered declaration names, deduplicated and sorted by Name.lt. Lookup order is independent of attribute and import order.

Equations

• Hex.RCF.handlerNames = do let __do_lift ← Lean.getEnv pure ((Hex.RCF.handlerExt✝.getState __do_lift).qsort Lean.Name.lt).eraseReps

def Hex.RCF.checkAxioms (name : Lean.Name) (proof : Lean.Expr) : Lean.MetaM Unit

Optional solvers may depend only on Lean's standard logical axioms. Imported dependency inventories also cover theorem bodies hidden by modules.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RCF.checkExpr (name : Lean.Name) (expression : Lean.Expr) : Lean.MetaM Lean.Expr

Screen closed expression data before native evaluation or proof acceptance. Local hypotheses remain permitted; unresolved and nonstandard dependencies do not.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RCF.checkProof (name : Lean.Name) (target proof : Lean.Expr) (category : String := "rcf proof") : Lean.MetaM Lean.Expr

Accept only a closed ordinary proof of the exact target. Agreement cannot assign caller metavariables; a fresh uncached theorem checks the candidate against its target in the kernel and exposes all transitive dependencies.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RCF.proveRationalGoal (target : Lean.Expr) : Lean.MetaM Lean.Expr

Prove a rational goal without dispatching coefficient handlers. Unsupported syntax and unsuccessful proof attempts restore the metavariable state.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RCF.proveGoal (target : Lean.Expr) : Lean.MetaM Lean.Expr

Prove a rational goal, or dispatch only a typed closed-coefficient decline. Every unsuccessful attempt restores its metavariable state, including runtime exceptions. Existing rational search and replay remain terminal.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RCF.rcfTac : Lean.ParserDescr

Decide a supported singly quantified univariate real polynomial goal by building and replaying a literal certificate.

Equations

• Hex.RCF.rcfTac = Lean.ParserDescr.node `Hex.RCF.rcfTac 1024 (Lean.ParserDescr.nonReservedSymbol "rcf" false)

def Hex.RCF.evalRCFTac : Lean.Elab.Tactic.Tactic

Elaborate rcf by constructing and replaying a checked certificate.

Equations

• One or more equations did not get rendered due to their size.