inductive Aesop.UnfoldResult (α : Type) : Type

• unchanged: {α : Type} → Aesop.UnfoldResult α
• changed: {α : Type} → α → Lean.HashSet Lean.Name → Aesop.UnfoldResult α

def Aesop.UnfoldResult.new? {α : Type} : Aesop.UnfoldResult α → Option α

Equations

• x.new? = match x with | Aesop.UnfoldResult.unchanged => none | Aesop.UnfoldResult.changed x usedDecls => some x

def Aesop.UnfoldResult.usedDecls? {α : Type} : Aesop.UnfoldResult α → Option (Lean.HashSet Lean.Name)

Equations

• x.usedDecls? = match x with | Aesop.UnfoldResult.unchanged => none | Aesop.UnfoldResult.changed new usedDecls => some usedDecls

def Aesop.UnfoldResult.usedDecls {α : Type} (r : Aesop.UnfoldResult α) : Lean.HashSet Lean.Name

Equations

• r.usedDecls = r.usedDecls?.getD ∅

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Aesop.unfoldManyCore (ctx : Lean.Meta.Simp.Context) (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.HashSet Lean.Name) Lean.MetaM Lean.Meta.Simp.Result

Equations

• One or more equations did not get rendered due to their size.

def Aesop.unfoldManyCore.pre (unfold? : Lean.Name → Option (Option Lean.Name)) (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.HashSet Lean.Name) Lean.Meta.SimpM Lean.Meta.Simp.Step

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 (Aesop.UnfoldResult Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.unfoldManyStar (goal : Lean.MVarId) (unfold? : Lean.Name → Option (Option Lean.Name)) : Lean.MetaM (Aesop.UnfoldResult Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.«tacticAesop_unfold[_,,]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.