def Aesop.tacticAesop_cases_ : Lean.ParserDescr

Equations

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

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

• Aesop.UnfoldResult.new? x = 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

• Aesop.UnfoldResult.usedDecls? x = 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

• 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.

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