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.