def
Aesop.RuleTac.applyExpr'
(goal : Lean.MVarId)
(e : Lean.Expr)
(eStx : Lean.Term)
(patSubst? : Option Substitution)
(md : Lean.Meta.TransparencyMode)
:
Equations
Instances For
def
Aesop.RuleTac.applyExpr
(goal : Lean.MVarId)
(e : Lean.Expr)
(eStx : Lean.Term)
(patSubsts? : Option (Std.HashSet Substitution))
(md : Lean.Meta.TransparencyMode)
: