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
🔸 coverage
def Mathlib.Tactic.Bound.isZero {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) :
Lean.MetaM Bool

Check if an expression is zero

Instances For
    source
    🔸 coverage
    def Mathlib.Tactic.Bound.ineqPriority {u : Lean.Level} {α : Q(Type u)} (a b : Q(«$α»)) :
    Lean.MetaM â„•

    Map the arguments of an inequality expression to a score

    Instances For
      source
      🔸 coverage
      partial def Mathlib.Tactic.Bound.hypPriority (hyp : Q(Prop)) :
      Lean.MetaM â„•

      Map a hypothesis type to a score

      source
      🔸 coverage
      def Mathlib.Tactic.Bound.typePriority (decl : Lean.Name) (type : Lean.Expr) :
      Lean.MetaM â„•

      Map a type to a score

      Instances For
        source
        🔸 coverage
        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)

        Instances For
          source
          🔸 coverage
          def Mathlib.Tactic.Bound.scoreToConfig (decl : Lean.Name) (score : â„•) :
          Aesop.Frontend.RuleConfig

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

          Instances For
            source
            🔸 coverage
            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.

            Instances For