def Aesop.RuleTac.applyExpr' (goal : Lean.MVarId) (e : Lean.Expr) (eStx : Lean.Term) (pat? : Option Aesop.RulePattern) (patInst : Aesop.RulePatternInstantiation) (md : Lean.Meta.TransparencyMode) : Lean.MetaM Aesop.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) (pat? : Option Aesop.RulePattern) (patInsts : Std.HashSet Aesop.RulePatternInstantiation) (md : Lean.Meta.TransparencyMode) : Lean.MetaM Aesop.RuleTacOutput

Equations

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

def Aesop.RuleTac.applyConst (decl : Lean.Name) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

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

def Aesop.RuleTac.applyTerm (stx : Lean.Term) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

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

def Aesop.RuleTac.apply (t : Aesop.RuleTerm) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTac

Equations

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

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

Equations

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