Documentation

Aesop.Script.UScriptToSScript

source
inductive Aesop.Script.StepTree :
Type
Instances For
    source
    instance Aesop.Script.instNonemptyStepTree :
    Nonempty StepTree
    source
    partial def Aesop.Script.StepTree.toMessageData? :
    StepTree → Option Lean.MessageData
    source
    def Aesop.Script.StepTree.toMessageData (t : StepTree) :
    Lean.MessageData
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.Script.instToMessageDataStepTree :
      Lean.ToMessageData StepTree
      source
      def Aesop.Script.UScript.toStepTree (s : UScript) :
      StepTree
      Instances For
        source
        def Aesop.Script.sortDedupArrays {α : Type u_1} [Ord α] (as : Array (Array α)) :
        Array α
        Instances For
          source
          def Aesop.Script.isConsecutiveSequence (ns : Array Nat) :
          Bool
          Instances For
            source
            def Aesop.Script.StepTree.focusableGoals (t : StepTree) :
            Std.HashMap Lean.MVarId Nat
            Instances For
              source
              def Aesop.Script.StepTree.numSiblings (t : StepTree) :
              Std.HashMap Lean.MVarId Nat
              Instances For
                source
                def Aesop.Script.orderedUScriptToSScript (uscript : UScript) (tacticState : TacticState) :
                Lean.CoreM SScript
                Instances For