Documentation

Aesop.Tree.ExtractScript

source
structure Aesop.ExtractScriptM.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Aesop.ExtractScriptM (α : Type) :
    Type
    Instances For
      source
      def Aesop.ExtractScriptM.run {α : Type} (x : ExtractScriptM α) :
      TreeM (Script.UScript × Bool)
      Instances For
        source
        def Aesop.ExtractScript.lazyStepToStep (ruleName : DisplayRuleName) (lstep : Script.LazyStep) :
        Lean.MetaM Script.Step
        Instances For
          source
          def Aesop.ExtractScript.lazyStepsToSteps (ruleName : DisplayRuleName) :
          Option (Array Script.LazyStep) → Lean.MetaM (Array Script.Step)
          Instances For
            source
            def Aesop.ExtractScript.recordStep (step : Script.Step) :
            ExtractScriptM Unit
            Instances For
              source
              def Aesop.ExtractScript.recordLazySteps (ruleName : DisplayRuleName) (steps? : Option (Array Script.LazyStep)) :
              ExtractScriptM Unit
              Instances For
                source
                def Aesop.ExtractScript.visitGoal (g : Goal) :
                ExtractScriptM Unit
                Instances For
                  source
                  def Aesop.ExtractScript.visitRapp (r : Rapp) :
                  ExtractScriptM Unit
                  Instances For
                    source
                    partial def Aesop.MVarClusterRef.extractScriptCore (cref : MVarClusterRef) :
                    ExtractScriptM Unit
                    source
                    partial def Aesop.GoalRef.extractScriptCore (gref : GoalRef) :
                    ExtractScriptM Unit
                    source
                    partial def Aesop.RappRef.extractScriptCore (rref : RappRef) :
                    ExtractScriptM Unit
                    source
                    @[inline]
                    def Aesop.extractScript :
                    TreeM (Script.UScript × Bool)
                    Instances For
                      source
                      def Aesop.MVarClusterRef.extractSafePrefixScriptCore (mref : MVarClusterRef) :
                      ExtractScriptM Unit
                      Instances For
                        source
                        partial def Aesop.GoalRef.extractSafePrefixScriptCore (gref : GoalRef) :
                        ExtractScriptM Unit
                        source
                        partial def Aesop.RappRef.extractSafePrefixScriptCore (rref : RappRef) :
                        ExtractScriptM Unit
                        source
                        def Aesop.extractSafePrefixScript :
                        TreeM (Script.UScript × Bool)
                        Instances For