Documentation

Aesop.Script.Check

source
def Aesop.Script.UScript.checkIfEnabled (uscript : UScript) :
Lean.MetaM Unit
Equations
    Instances For
      source
      def Aesop.checkRenderedScriptIfEnabled (script : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) (expectCompleteProof : Bool) :
      Lean.MetaM Unit
      Equations
        Instances For