Public API

The LeanCert namespace re-exports the most commonly used definitions so users can write open LeanCert and have immediate access to the core API.

Convenience abbreviations

@[reducible, inline]

noncomputable abbrev LeanCert.eval₀ (e : Expr) (x : ℝ) : ℝ

Evaluate a single-variable expression at a real point. Shorthand for Expr.eval (fun _ => x) e.

Equations

• LeanCert.eval₀ e x = LeanCert.Core.Expr.eval (fun (x_1 : ℕ) => x) e

def LeanCert.eval₀_rat (e : Expr) (x : ℚ) : ℚ

Evaluate a single-variable expression at a rational point. Useful for #eval demonstrations.

Equations

• LeanCert.eval₀_rat (LeanCert.Core.Expr.const q) x = q
• LeanCert.eval₀_rat (LeanCert.Core.Expr.var idx) x = x
• LeanCert.eval₀_rat (e₁.add e₂) x = LeanCert.eval₀_rat e₁ x + LeanCert.eval₀_rat e₂ x
• LeanCert.eval₀_rat (e₁.mul e₂) x = LeanCert.eval₀_rat e₁ x * LeanCert.eval₀_rat e₂ x
• LeanCert.eval₀_rat e_2.neg x = -LeanCert.eval₀_rat e_2 x
• LeanCert.eval₀_rat e_2.inv x = (LeanCert.eval₀_rat e_2 x)⁻¹
• LeanCert.eval₀_rat e_2.exp x = 0
• LeanCert.eval₀_rat e_2.sin x = 0
• LeanCert.eval₀_rat e_2.cos x = 0
• LeanCert.eval₀_rat e_2.log x = 0
• LeanCert.eval₀_rat e_2.atan x = 0
• LeanCert.eval₀_rat e_2.arsinh x = 0
• LeanCert.eval₀_rat e_2.atanh x = 0
• LeanCert.eval₀_rat e_2.sinc x = 0
• LeanCert.eval₀_rat e_2.erf x = 0
• LeanCert.eval₀_rat e_2.sinh x = 0
• LeanCert.eval₀_rat e_2.cosh x = 0
• LeanCert.eval₀_rat e_2.tanh x = 0
• LeanCert.eval₀_rat e_2.sqrt x = 0
• LeanCert.eval₀_rat LeanCert.Core.Expr.pi x = 157 / 50

def LeanCert.unitInterval : IntervalRat

The unit interval [0, 1]

Equations

• LeanCert.unitInterval = { lo := 0, hi := 1, le := LeanCert.unitInterval._proof_1 }

def LeanCert.symInterval : IntervalRat

The interval [-1, 1]

Equations

• LeanCert.symInterval = { lo := -1, hi := 1, le := LeanCert.symInterval._proof_1 }