Documentation

Aesop.Util.Tactic.Unfold

source
def Aesop.mkUnfoldSimpContext :
Lean.MetaM Lean.Meta.Simp.Context
Equations
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.
source
def Aesop.unfoldMany (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Array Lean.Name))
Equations
  • One or more equations did not get rendered due to their size.
source
def Aesop.unfoldManyTarget (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
Lean.MetaM (Option (Lean.MVarId × Array Lean.Name))
Equations
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.
source
def Aesop.unfoldManyStar (unfold? : Lean.Name → Option (Option Lean.Name)) (goal : Lean.MVarId) :
Lean.MetaM (Option Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
def Aesop.tacticAesop_unfold_ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Aesop.tacticAesop_unfold_At_ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.