@[inline, reducible]

abbrev Aesop.ExtractScriptM (α : Type) : Type

Equations

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

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

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

@[always_inline]

def Aesop.GoalRef.extractScriptCore.getNormScript (gid : Aesop.GoalId) : Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.ExtractScriptM Aesop.UnstructuredScript

Equations

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

partial def Aesop.RappRef.extractScriptCore (rref : Aesop.RappRef) (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) : Aesop.ExtractScriptM Unit

@[inline]

def Aesop.MVarClusterRef.extractScript (cref : Aesop.MVarClusterRef) : Aesop.TreeM Aesop.UnstructuredScript

Equations

• Aesop.MVarClusterRef.extractScript cref = (fun (x : Unit × Aesop.UnstructuredScript) => x.snd) <$> StateRefT'.run (Aesop.MVarClusterRef.extractScriptCore cref) #[]