Documentation

Mathlib.Tactic.Linarith.NNRealPreprocessor

NNReal linarith preprocessing #

This file contains a linarith preprocessor for converting (in)equalities in ℝ≥0 to ℝ.

By overriding the behaviour of the placeholder preprocessor nnrealToReal (which does nothing unless this file is imported) linarith can still be used without importing NNReal.

source
def Mathlib.Tactic.Linarith.isNNRealProp (e : Lean.Expr) :
Lean.MetaM Bool

isNNRealProp tp is true iff tp is an inequality or equality between nonnegative real numbers or the negation thereof.

Instances For
    source
    def Mathlib.Tactic.Linarith.isNNRealtoReal (e : Lean.Expr) :
    Option Lean.Expr

    If e is of the form ((x : ℝ≥0) : ℝ), NNReal.toReal e returns x.

    Instances For
      source
      partial def Mathlib.Tactic.Linarith.getNNRealCoes (e : Lean.Expr) :
      List Lean.Expr

      getNNRealComparisons e returns a list of all subexpressions of e of the form (x : ℝ).

      source
      def Mathlib.Tactic.Linarith.mk_toReal_nonneg_prf (e : Lean.Expr) :
      Lean.MetaM (Option Lean.Expr)

      If e : ℝ≥0, returns a proof of 0 ≤ (e : ℝ).

      Instances For