@[reducible, inline]
Instances For
@[always_inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Aesop.RappRef.extractScriptCore
(rref : Aesop.RappRef)
(preGoal : Lean.MVarId)
(preState : Lean.Meta.SavedState)
:
@[inline]
Equations
- cref.extractScript = (fun (x : Unit × Aesop.UnstructuredScript) => x.snd) <$> StateRefT'.run cref.extractScriptCore #[]