def Aesop.tacticAesop_cases_ : Lean.ParserDescr

Equations

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

inductive Aesop.UnfoldResult : Type

• unchanged: Aesop.UnfoldResult
• changed: Lean.MVarId → Lean.HashSet Lean.Name → Aesop.UnfoldResult

def Aesop.UnfoldResult.newGoal? : Aesop.UnfoldResult → Option Lean.MVarId

Equations

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

def Aesop.UnfoldResult.usedDecls? : Aesop.UnfoldResult → Option (Lean.HashSet Lean.Name)

Equations

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

def Aesop.UnfoldResult.usedDecls (r : Aesop.UnfoldResult) : Lean.HashSet Lean.Name

Equations

• Aesop.UnfoldResult.usedDecls r = Option.getD (Aesop.UnfoldResult.usedDecls? r) ∅

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

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

Equations

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

@[inline]

def Aesop.unfoldManyStar.unfold (unfold? : Lean.Name → Option (Option Lean.Name)) (usedDecls : IO.Ref (Lean.HashSet Lean.Name)) (ctx : Lean.Meta.Simp.Context) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Aesop.unfoldManyStar.pre (unfold? : Lean.Name → Option (Option Lean.Name)) (usedDecls : IO.Ref (Lean.HashSet Lean.Name)) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

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.