Documentation

Aesop.Tree.ExtractScript

source
structure Aesop.ExtractScriptM.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Aesop.ExtractScriptM (α : Type) :
    Type
    Equations
      Instances For
        source
        def Aesop.ExtractScriptM.run {α : Type} (x : ExtractScriptM α) :
        TreeM (Script.UScript × Bool)
        Equations
          Instances For
            source
            def Aesop.ExtractScript.lazyStepToStep (ruleName : DisplayRuleName) (lstep : Script.LazyStep) :
            Lean.MetaM Script.Step
            Equations
              Instances For
                source
                def Aesop.ExtractScript.lazyStepsToSteps (ruleName : DisplayRuleName) :
                Option (Array Script.LazyStep) → Lean.MetaM (Array Script.Step)
                Equations
                  Instances For
                    source
                    def Aesop.ExtractScript.recordStep (step : Script.Step) :
                    ExtractScriptM Unit
                    Equations
                      Instances For
                        source
                        def Aesop.ExtractScript.recordLazySteps (ruleName : DisplayRuleName) (steps? : Option (Array Script.LazyStep)) :
                        ExtractScriptM Unit
                        Equations
                          Instances For
                            source
                            def Aesop.ExtractScript.visitGoal (g : Goal) :
                            ExtractScriptM Unit
                            Equations
                              Instances For
                                source
                                def Aesop.ExtractScript.visitRapp (r : Rapp) :
                                ExtractScriptM Unit
                                Equations
                                  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)
                                    Equations
                                      Instances For
                                        source
                                        def Aesop.MVarClusterRef.extractSafePrefixScriptCore (mref : MVarClusterRef) :
                                        ExtractScriptM Unit
                                        Equations
                                          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)
                                            Equations
                                              Instances For