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.

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.

Equations

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

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

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

Equations

• Mathlib.Tactic.Linarith.isNNRealtoReal ((Lean.Expr.const `NNReal.toReal us).app n) = some n
• Mathlib.Tactic.Linarith.isNNRealtoReal e = none

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 : ℝ).

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 : ℝ).

Equations

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