structure Aesop.ExtractScriptM.State : Type

• script : Aesop.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 : Aesop.ExtractScriptM α) : Aesop.TreeM (Aesop.Script.UScript × Bool)

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.ExtractScript.lazyStepsToSteps ruleName (some lsteps) = Array.mapM (Aesop.ExtractScript.lazyStepToStep ruleName) lsteps

def Aesop.ExtractScript.recordStep (step : Aesop.Script.Step) : Aesop.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 : Aesop.DisplayRuleName) (steps? : Option (Array Aesop.Script.LazyStep)) : Aesop.ExtractScriptM Unit

Equations

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

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

Equations

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

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

Equations

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

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

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

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

@[inline]

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

Equations

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

def Aesop.MVarClusterRef.extractSafePrefixScriptCore (mref : Aesop.MVarClusterRef) : Aesop.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 : Aesop.GoalRef) : Aesop.ExtractScriptM Unit

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

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

Equations

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