def Aesop.mkUnfoldSimpContext : Lean.MetaM Lean.Meta.Simp.Context

Equations

• Aesop.mkUnfoldSimpContext = do let __do_lift ← liftM Lean.Meta.getSimpCongrTheorems Lean.Meta.Simp.mkContext Lean.Meta.Simp.neutralConfig #[] __do_lift

@[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.

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.

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.

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.

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.