@[reducible, inline]
Equations
Instances For
Equations
- Aesop.ExtractScriptM.run completeProof x = (fun (x : α × Aesop.ExtractScriptM.State) => x.snd.script) <$> (ReaderT.run x { completeProof := completeProof }).run { script := #[] }
Instances For
def
Aesop.ExtractScript.lazyStepToStep
(ruleName : Aesop.DisplayRuleName)
(lstep : Aesop.Script.LazyStep)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.ExtractScript.recordStep step = modify fun (s : Aesop.ExtractScriptM.State) => { script := Array.push s.script step }
Instances For
def
Aesop.ExtractScript.recordLazySteps
(ruleName : Aesop.DisplayRuleName)
(steps? : Option (Array Aesop.Script.LazyStep))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
- Aesop.extractScript = do let __do_lift ← Aesop.getRootGoal Aesop.ExtractScriptM.run true __do_lift.extractScriptCore
Instances For
Equations
- mref.extractSafePrefixScriptCore = do let __do_lift ← ST.Ref.get mref Array.forM (fun (x : Aesop.GoalRef) => x.extractSafePrefixScriptCore) __do_lift.goals 0
Instances For
Equations
- Aesop.extractSafePrefixScript = do let __do_lift ← Aesop.getRootGoal Aesop.ExtractScriptM.run false __do_lift.extractSafePrefixScriptCore