structure Aesop.ExtractScriptM.Context : Type

• completeProof : Bool

structure Aesop.ExtractScriptM.State : Type

• script : Aesop.Script.UScript

@[reducible, inline]

abbrev Aesop.ExtractScriptM (α : Type) : Type

Equations

• Aesop.ExtractScriptM = ReaderT Aesop.ExtractScriptM.Context (StateRefT' IO.RealWorld Aesop.ExtractScriptM.State Aesop.TreeM)

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

Equations

• Aesop.ExtractScriptM.run completeProof x = (fun (x : α × Aesop.ExtractScriptM.State) => x.snd.script) <$> (ReaderT.run x { completeProof := completeProof }).run { script := #[] }

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.

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 }

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

Equations

• Aesop.extractScript = do let __do_lift ← Aesop.getRootGoal Aesop.ExtractScriptM.run true __do_lift.extractScriptCore

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 0

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

Equations

• Aesop.extractSafePrefixScript = do let __do_lift ← Aesop.getRootGoal Aesop.ExtractScriptM.run false __do_lift.extractSafePrefixScriptCore