def Aesop.RuleTac.applyExpr' (goal : Lean.MVarId) (e : Lean.Expr) (eStx : Lean.Term) (patSubst? : Option Substitution) (md : Lean.Meta.TransparencyMode) : BaseM RuleApplication

Equations

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

def Aesop.RuleTac.applyExpr (goal : Lean.MVarId) (e : Lean.Expr) (eStx : Lean.Term) (patSubsts? : Option (Std.HashSet Substitution)) (md : Lean.Meta.TransparencyMode) : BaseM RuleTacOutput

Equations

• One or more equations did not get rendered due to their size.
• Aesop.RuleTac.applyExpr goal e eStx patSubsts? md = do let rapp ← Aesop.RuleTac.applyExpr' goal e eStx none md pure { applications := #[rapp] }

def Aesop.RuleTac.applyConst (decl : Lean.Name) (md : Lean.Meta.TransparencyMode) : RuleTac

Equations

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

def Aesop.RuleTac.applyTerm (stx : Lean.Term) (md : Lean.Meta.TransparencyMode) : RuleTac

Equations

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

def Aesop.RuleTac.apply (t : RuleTerm) (md : Lean.Meta.TransparencyMode) : RuleTac

Equations

• Aesop.RuleTac.apply (Aesop.RuleTerm.const decl) md = Aesop.RuleTac.applyConst decl md
• Aesop.RuleTac.apply (Aesop.RuleTerm.term tm) md = Aesop.RuleTac.applyTerm tm md

def Aesop.RuleTac.applyConsts (decls : Array Lean.Name) (md : Lean.Meta.TransparencyMode) : RuleTac

Equations

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