Documentation

Mathlib.Tactic.Bound.Attribute

The bound attribute #

Any lemma tagged with @[bound] is registered as an apply rule for the bound tactic, by converting it to either norm apply or safe apply <priority>. The classification is based on the number and types of the lemma's hypotheses.

source
def Mathlib.Tactic.Bound.isZero {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) :
Lean.MetaM Bool

Check if an expression is zero

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Bound.ineqPriority {u : Lean.Level} {α : Q(Type u)} (a : Q(«$α»)) (b : Q(«$α»)) :
Lean.MetaM ℕ

Map the arguments of an inequality expression to a score

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Mathlib.Tactic.Bound.hypPriority (hyp : Q(Prop)) :
Lean.MetaM ℕ

Map a hypothesis type to a score

source
def Mathlib.Tactic.Bound.typePriority (decl : Lean.Name) (type : Lean.Expr) :
Lean.MetaM ℕ

Map a type to a score

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Bound.typePriority.argPriority (x : Lean.Expr) :
Lean.MetaM ℕ

Score the type of argument x

Equations
source
def Mathlib.Tactic.Bound.typePriority.checkResult (decl : Lean.Name) (type : Lean.Expr) (t : Q(Prop)) :
Lean.MetaM Unit

Insist that our conclusion is an inequality

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Bound.declPriority (decl : Lean.Name) :
Lean.MetaM ℕ

Map a theorem decl to a score (0 means norm apply, 0 < means safe apply)

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Bound.scoreToConfig (decl : Lean.Name) (score : ℕ) :
Aesop.Frontend.RuleConfig

Map a score to either norm apply or safe apply <priority>

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.Bound.attrBound_forward :
Lean.ParserDescr

Attribute for forward rules for the bound tactic.

@[bound_forward] lemmas should produce inequalities given other hypotheses that might be in the context. A typical example is exposing an inequality field of a structure, such as HasPowerSeriesOnBall.r_pos.

Equations