structure Aesop.ExtractScriptM.State : Type

• script : Script.UScript
• proofHasMVar : Bool

@[reducible, inline]

abbrev Aesop.ExtractScriptM (α : Type) : Type

Equations

• Aesop.ExtractScriptM = StateRefT' IO.RealWorld Aesop.ExtractScriptM.State Aesop.TreeM

def Aesop.ExtractScriptM.run {α : Type} (x : ExtractScriptM α) : TreeM (Script.UScript × Bool)

Equations

• x.run = do let __discr ← StateRefT'.run x { } match __discr with | (fst, r) => pure (r.script, r.proofHasMVar)

def Aesop.ExtractScript.lazyStepToStep (ruleName : DisplayRuleName) (lstep : Script.LazyStep) : Lean.MetaM Script.Step

Equations

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

def Aesop.ExtractScript.lazyStepsToSteps (ruleName : DisplayRuleName) : Option (Array Script.LazyStep) → Lean.MetaM (Array Script.Step)

Equations

• Aesop.ExtractScript.lazyStepsToSteps ruleName none = Lean.throwError (Lean.toMessageData "tactic script generation is not supported by rule " ++ Lean.toMessageData ruleName)
• Aesop.ExtractScript.lazyStepsToSteps ruleName (some lsteps) = Array.mapM (Aesop.ExtractScript.lazyStepToStep ruleName) lsteps

def Aesop.ExtractScript.recordStep (step : Script.Step) : ExtractScriptM Unit

Equations

• Aesop.ExtractScript.recordStep step = modify fun (s : Aesop.ExtractScriptM.State) => { script := Array.push s.script step, proofHasMVar := s.proofHasMVar }

def Aesop.ExtractScript.recordLazySteps (ruleName : DisplayRuleName) (steps? : Option (Array Script.LazyStep)) : ExtractScriptM Unit

Equations

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

def Aesop.ExtractScript.visitGoal (g : Goal) : ExtractScriptM Unit

Equations

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

def Aesop.ExtractScript.visitRapp (r : Rapp) : ExtractScriptM Unit

Equations

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

partial def Aesop.MVarClusterRef.extractScriptCore (cref : MVarClusterRef) : ExtractScriptM Unit

partial def Aesop.GoalRef.extractScriptCore (gref : GoalRef) : ExtractScriptM Unit

partial def Aesop.RappRef.extractScriptCore (rref : RappRef) : ExtractScriptM Unit

@[inline]

def Aesop.extractScript : TreeM (Script.UScript × Bool)

Equations

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

def Aesop.MVarClusterRef.extractSafePrefixScriptCore (mref : MVarClusterRef) : ExtractScriptM Unit

Equations

• mref.extractSafePrefixScriptCore = do let __do_lift ← ST.Ref.get mref Array.forM (fun (x : Aesop.GoalRef) => x.extractSafePrefixScriptCore) __do_lift.goals

partial def Aesop.GoalRef.extractSafePrefixScriptCore (gref : GoalRef) : ExtractScriptM Unit

partial def Aesop.RappRef.extractSafePrefixScriptCore (rref : RappRef) : ExtractScriptM Unit

def Aesop.extractSafePrefixScript : TreeM (Script.UScript × Bool)

Equations

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