Documentation

Aesop.Util.Tactic.Unfold

source
def Aesop.mkUnfoldSimpContext :
Lean.MetaM Lean.Meta.Simp.Context
Equations
    Instances For
      source
      @[inline]
      def Aesop.unfoldManyCore (ctx : Lean.Meta.Simp.Context) (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) :
      StateRefT' IO.RealWorld (Array Lean.Name) Lean.MetaM Lean.Meta.Simp.Result
      Equations
        Instances For
          source
          def Aesop.unfoldManyCore.pre (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) :
          StateRefT' IO.RealWorld (Array Lean.Name) Lean.Meta.SimpM Lean.Meta.Simp.Step
          Equations
            Instances For
              source
              def Aesop.unfoldMany (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) :
              Lean.MetaM (Option (Lean.Expr × Array Lean.Name))
              Equations
                Instances For
                  source
                  def Aesop.unfoldManyTarget (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
                  Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
                  Equations
                    Instances For
                      source
                      def Aesop.unfoldManyAt (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) (fvarId : Lean.FVarId) :
                      Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
                      Equations
                        Instances For
                          source
                          def Aesop.unfoldManyStar (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
                          Lean.MetaM (Option Lean.MVarId)
                          Equations
                            Instances For
                              source
                              def Aesop.tacticAesop_unfold_ :
                              Lean.ParserDescr
                              Equations
                                Instances For
                                  source
                                  def Aesop.tacticAesop_unfold_At_ :
                                  Lean.ParserDescr
                                  Equations
                                    Instances For