Documentation

Aesop.Util.Unfold

source
def Aesop.mkUnfoldSimpContext :
Lean.MetaM Lean.Meta.Simp.Context
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
    Instances For
      source
      def Aesop.unfoldMany (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) :
      Lean.MetaM (Option (Lean.Expr × Array Lean.Name))
      Instances For
        source
        def Aesop.unfoldManyTarget (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
        Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
        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))
          Instances For
            source
            def Aesop.unfoldManyStar (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
            Lean.MetaM (Option Lean.MVarId)
            Instances For