# Documentation

Mathlib.Tactic.NormNum.Core

## norm_num core functionality #

This file sets up the norm_num tactic and the @[norm_num] attribute, which allow for plugging in new normalization functionality around a simp-based driver. The actual behavior is in @[norm_num]-tagged definitions in Tactic.NormNum.Basic and elsewhere.

Attribute for identifying norm_num extensions.

Equations
• One or more equations did not get rendered due to their size.
structure Mathlib.Meta.NormNum.IsNat {α : Type u_1} [inst : ] (a : α) (n : ) :
• The element is equal to the coercion of the natural number.

out : a = n

Assert that an element of a semiring is equal to the coercion of some natural number.

Instances For
def Nat.rawCast {α : Type u_1} [inst : ] (n : ) :
α

A "raw nat cast" is an expression of the form (Nat.rawCast lit : α) where lit is a raw natural number literal. These expressions are used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

Equations
• = n
theorem Mathlib.Meta.NormNum.IsNat.to_eq {α : Type u_1} [inst : ] {n : } {a : α} {a' : α} :
n = a'a = a'
theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq {α : Type u_1} {a : α} {n : } [inst : ] :
a =
theorem Mathlib.Meta.NormNum.IsNat.of_raw (α : Type u_1) [inst : ] (n : ) :
structure Mathlib.Meta.NormNum.IsInt {α : Type u_1} [inst : Ring α] (a : α) (n : ) :
• The element is equal to the coercion of the integer.

out : a = n

Assert that an element of a ring is equal to the coercion of some integer.

Instances For
def Int.rawCast {α : Type u_1} [inst : Ring α] (n : ) :
α

A "raw int cast" is an expression of the form:

• (Nat.rawCast lit : α) where lit is a raw natural number literal
• (Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal

(That is, we only actually use this function for negative integers.) This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

Equations
• = n
theorem Mathlib.Meta.NormNum.IsInt.to_isNat {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsNat.to_isInt {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq {α : Type u_1} {a : α} {n : } [inst : Ring α] :
a =
theorem Mathlib.Meta.NormNum.IsInt.of_raw (α : Type u_1) [inst : Ring α] (n : ) :
theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq {α : Type u_1} [inst : Ring α] {n : } {a : α} {a' : α} :
n = a'a = -a'
theorem Mathlib.Meta.NormNum.IsInt.nonneg_to_eq {α : Type u_1} [inst : Ring α] {n : } {a : α} {a' : α} (h : ) (e : n = a') :
a = a'

Represent an integer as a typed expression.

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

A shortcut (non)instance for AddMonoidWithOne ℕ to shrink generated proofs.

Equations

A shortcut (non)instance for Ring ℤ to shrink generated proofs.

Equations
inductive Mathlib.Meta.NormNum.IsRat {α : Type u_1} [inst : Ring α] (a : α) (num : ) (denom : ) :

Assert that an element of a ring is equal to num / denom (and denom is invertible so that this makes sense). We will usually also have num and denom coprime, although this is not part of the definition.

Instances For
def Rat.rawCast {α : Type u_1} [inst : ] (n : ) (d : ) :
α

A "raw rat cast" is an expression of the form:

• (Nat.rawCast lit : α) where lit is a raw natural number literal
• (Int.rawCast (Int.negOfNat lit) : α) where lit is a nonzero raw natural number literal
• (Rat.rawCast n d : α) where n is a raw int cast, d is a raw nat cast, and d is not 1 or 0.

This representation is used by tactics like ring to decrease the number of typeclass arguments required in each use of a number literal at type α.

Equations
• = n / d
theorem Mathlib.Meta.NormNum.IsRat.to_isNat {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsNat.to_isRat {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsRat.to_isInt {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsInt.to_isRat {α : Type u_1} [inst : Ring α] {a : α} {n : } :
theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq {α : Type u_1} {n : } {d : } [inst : ] {a : α} :
a =
theorem Mathlib.Meta.NormNum.IsRat.neg_to_eq {α : Type u_1} [inst : ] {n : } {d : } {a : α} {n' : α} {d' : α} :
n = n'd = d'a = -(n' / d')
theorem Mathlib.Meta.NormNum.IsRat.nonneg_to_eq {α : Type u_1} [inst : ] {n : } {d : } {a : α} {n' : α} {d' : α} :
n = n'd = d'a = n' / d'
theorem Mathlib.Meta.NormNum.IsRat.of_raw (α : Type u_1) [inst : ] (n : ) (d : ) (h : d 0) :
theorem Mathlib.Meta.NormNum.IsRat.den_nz {α : Type u_1} [inst : ] {a : α} {n : } {d : } :
d 0

Represent an integer as a typed expression.

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

A shortcut (non)instance for Ring ℚ to shrink generated proofs.

Equations

A shortcut (non)instance for DivisionRing ℚ to shrink generated proofs.

Equations
• Untyped version of Result.isBool.

isBool:
• Untyped version of Result.isNat.

isNat:
• Untyped version of Result.isNegNat.

isNegNat:
• Untyped version of Result.isRat.

isRat:

The result of norm_num running on an expression x of type α. Untyped version of Result.

Instances For
def Mathlib.Meta.NormNum.Result {u : Lean.Level} {α : } (x : ) :

The result of norm_num running on an expression x of type α.

Equations
instance Mathlib.Meta.NormNum.instInhabitedResult :
{a : Lean.Level} → {α : Q(Type a)} → {x : Q(«$α»)} → Equations • Mathlib.Meta.NormNum.instInhabitedResult = @[match_pattern, inline] def Mathlib.Meta.NormNum.Result.isTrue {x : Q(Prop)} (proof : ) : The result is proof : x, where x is a (true) proposition. Equations • Mathlib.Meta.NormNum.Result.isTrue = @[match_pattern, inline] The result is proof : ¬x¬x, where x is a (false) proposition. Equations • Mathlib.Meta.NormNum.Result.isFalse = @[match_pattern, inline] def Mathlib.Meta.NormNum.Result.isNat {u : Lean.Level} {α : } {x : } (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const AddMonoidWithOne [u]) α)) _auto✝) (lit : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsNat [u]) α) inst) x) lit)) : The result is lit : ℕ (a raw nat literal) and proof : isNat x lit. Equations @[match_pattern, inline] def Mathlib.Meta.NormNum.Result.isNegNat {u : Lean.Level} {α : } {x : } (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) (lit : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) (Lean.Expr.app (Lean.Expr.const Int.negOfNat []) lit))) : The result is -lit where lit is a raw nat literal and proof : isInt x (.negOfNat lit). Equations @[match_pattern, inline] def Mathlib.Meta.NormNum.Result.isRat {u : Lean.Level} {α : } {x : } (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) (q : ) (n : Q()) (d : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) inst)) x) n) d)) : The result is proof : isRat x n d, where n is either .ofNat lit or .negOfNat lit with lit a raw nat literal and d is a raw nat literal (not 0 or 1), and q is the value of n / d. Equations A shortcut (non)instance for AddMonoidWithOne α from Ring α to shrink generated proofs. Equations • Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance def Mathlib.Meta.NormNum.Result.isInt {u : Lean.Level} {α : } {x : } (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) (z : Q()) (n : ) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) z)) : The result is z : ℤ and proof : isNat x z. Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.toRat : {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«$α»)} →

Returns the rational number that is the result of norm_num evaluation.

Equations
• One or more equations did not get rendered due to their size.
def Lean.LOption.toOption {α : Type u_1} :

Convert undef to none to make an LOption into an Option.

Equations
• = match x with | => some a | x => none

Helper function to synthesize a typed AddMonoidWithOne α expression.

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

Helper function to synthesize a typed Semiring α expression.

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

Helper function to synthesize a typed Ring α expression.

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

Helper function to synthesize a typed DivisionRing α expression.

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

Helper function to synthesize a typed OrderedSemiring α expression.

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

Helper function to synthesize a typed OrderedRing α expression.

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

Helper function to synthesize a typed LinearOrderedField α expression.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) :
Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Ring.toAddGroupWithOne [u]) α) _i))))

Helper function to synthesize a typed CharZero α expression given Ring α.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) :
Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Ring.toAddGroupWithOne [u]) α) _i)))))

Helper function to synthesize a typed CharZero α expression given Ring α, if it exists.

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

Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

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

Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α, if it exists.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) :
Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) _i)))))

Helper function to synthesize a typed CharZero α expression given DivisionRing α.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? {u : Lean.Level} {α : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) :
Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) _i))))))

Helper function to synthesize a typed CharZero α expression given DivisionRing α, if it exists.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.Result.toInt {u : Lean.Level} {α : } {e : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) :
Option ( × (lit : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsInt [u]) α) _i) e) lit))

Extract from a Result the integer value (as both a term and an expression), and the proof that the original expression is equal to this integer.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.Result.toRat' {u : Lean.Level} {α : } {e : } (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) :
Option ( × (n : Q()) × (d : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) _i)) e) n) d))

Extract from a Result the rational value (as both a term and an expression), and the proof that the original expression is equal to this rational number.

Equations
• One or more equations did not get rendered due to their size.
instance Mathlib.Meta.NormNum.instToMessageDataResult :
{a : Lean.Level} → {α : Q(Type a)} → {x : Q(«$α»)} → Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.toRawEq {u : Lean.Level} {α : } {e : } : (e' : ) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app () α) e) e') Given a NormNum.Result e (which uses IsNat, IsInt, IsRat to express equality to a rational numeral), converts it to an equality e = Nat.rawCast n, e = Int.rawCast n, or e = Rat.rawCast n d to a raw cast expression, so it can be used for rewriting. Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.toRawIntEq {u : Lean.Level} {α : } {e : } : Option ( × (e' : ) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app () α) e) e')) Result.toRawEq but providing an integer. Given a NormNum.Result e for something known to be an integer (which uses IsNat or IsInt to express equality to an integer numeral), converts it to an equality e = Nat.rawCast n or e = Int.rawCast n to a raw cast expression, so it can be used for rewriting. Gives none if not an integer. Equations • One or more equations did not get rendered due to their size. Constructs a Result out of a raw nat cast. Assumes e is a raw nat cast expression. Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.ofRawInt {u : Lean.Level} {α : } (n : ) (e : ) : Constructs a Result out of a raw int cast. Assumes e is a raw int cast expression denoting n. Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.ofRawRat {u : Lean.Level} {α : } (q : ) (e : ) (hyp : optParam () none) : Constructs a Result out of a raw rat cast. Assumes e is a raw rat cast expression denoting n. Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.isRat' {u : Lean.Level} {α : } {x : } (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) (q : ) (n : Q()) (d : Q()) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) inst)) x) n) d)) : The result depends on whether q : ℚ happens to be an integer, in which case the result is .isInt .. whereas otherwise it's .isRat ... Equations • One or more equations did not get rendered due to their size. def Mathlib.Meta.NormNum.Result.toRatNZ : {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«$α»)} →

Returns the rational number that is the result of norm_num evaluation, along with a proof that the denominator is nonzero in the isRat case.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.mkOfNat {u : Lean.Level} (α : ) (_sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const AddMonoidWithOne [u]) α)) (lit : Q()) :
Lean.MetaM ((a' : ) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app () α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const AddMonoidWithOne.toNatCast [u]) α) _sα)) lit)) a'))

Constructs an ofNat application a' with the canonical instance, together with a proof that the instance is equal to the result of Nat.cast on the given AddMonoidWithOne instance.

This function is performance-critical, as many higher level tactics have to construct numerals. So rather than using typeclass search we hardcode the (relatively small) set of solutions to the typeclass problem.

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

Convert a Result to a Simp.Result.

Equations
• One or more equations did not get rendered due to their size.
• The extension should be run in the pre phase when used as simp plugin.

pre : Bool
• The extension should be run in the post phase when used as simp plugin.

post : Bool
• Attempts to prove an expression is equal to some explicit number of the relevant type.

eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«\$α»)) →
• The name of the norm_num extension.

name :

A extension for norm_num.

Instances For

Read a norm_num extension from a declaration of the right type.

Equations
• = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept ())
@[inline]

Each norm_num extension is labelled with a collection of patterns which determine the expressions to which it should be applied.

Equations
• The tree of norm_num extensions.

• Erased norm_nums.

erased :

The state of the norm_num extension environment

Instances For
Equations

Environment extensions for norm_num declarations

def Mathlib.Meta.NormNum.derive {u : Lean.Level} {α : } (e : ) (post : ) :

Run each registered norm_num extension on an expression, returning a NormNum.Result.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.deriveNat' {u : Lean.Level} {α : } (e : ) :
Lean.MetaM ((_inst : Qq.QQ (Lean.Expr.app (Lean.Expr.const AddMonoidWithOne [u]) α)) × (lit : Qq.QQ (Lean.Expr.const Nat [])) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsNat [u]) α) _inst) e) lit))

Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℕ, and a proof of isNat e lit.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.deriveNat {u : Lean.Level} {α : } (e : ) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const AddMonoidWithOne [u]) α)) _auto✝) :
Lean.MetaM ((lit : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsNat [u]) α) _inst) e) lit))

Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℕ, and a proof of isNat e lit.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.deriveInt {u : Lean.Level} {α : } (e : ) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const Ring [u]) α)) _auto✝) :
Lean.MetaM ((lit : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsInt [u]) α) _inst) e) lit))

Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℤ, and a proof of IsInt e lit in expression form.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.deriveRat {u : Lean.Level} {α : } (e : ) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const DivisionRing [u]) α)) _auto✝) :
Lean.MetaM ( × (n : Q()) × (d : Q()) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const DivisionRing.toRing [u]) α) _inst)) e) n) d))

Run each registered norm_num extension on a typed expression e : α, returning a rational number, typed expressions n : ℚ and d : ℚ for the numerator and denominator, and a proof of IsRat e n d in expression form.

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

Extract the natural number n if the expression is of the form OfNat.ofNat n.

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

Extract the integer i if the expression is either a natural number literal or the negation of one.

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

Extract the numerator n : ℤ and denominator d : ℕ if the expression is either an integer literal, or the division of one integer literal by another.

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

Test if an expression represents an explicit number written in normal form.

Equations
def Mathlib.Meta.NormNum.eval (e : Lean.Expr) (post : ) :

Run each registered norm_num extension on an expression, returning a Simp.Result.

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

Erases a name marked norm_num by adding it to the state's erased field and removing it from the state's list of Entrys.

Equations
def Mathlib.Meta.NormNum.NormNums.erase {m : } [inst : ] [inst : ] (declName : Lean.Name) :

Erase a name marked as a norm_num attribute.

Check that it does in fact have the norm_num attribute by making sure it names a NormNumExt found somewhere in the state's tree, and is not erased.

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

A simp plugin which calls NormNum.eval.

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

Constructs a proof that the original expression is true given a simp result which simplifies the target to True.

Equations
• One or more equations did not get rendered due to their size.
partial def Mathlib.Meta.NormNum.discharge (ctx : Lean.Meta.Simp.Context) (useSimp : ) (e : Lean.Expr) :

A discharger which calls norm_num.

A Methods implementation which calls norm_num.

partial def Mathlib.Meta.NormNum.deriveSimp (ctx : Lean.Meta.Simp.Context) (useSimp : ) (e : Lean.Expr) :

Traverses the given expression using simp and normalises any numbers it finds.

def Mathlib.Meta.NormNum.normNumAt (g : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : ) (simplifyTarget : ) (useSimp : ) :

The core of norm_num as a tactic in MetaM.

• g: The goal to simplify
• ctx: The simp context, constructed by mkSimpContext and containing any additional simp rules we want to use
• fvarIdsToSimp: The selected set of hypotheses used in the location argument
• simplifyTarget: true if the target is selected in the location argument
• useSimp: true if we used norm_num instead of norm_num1
Equations
• One or more equations did not get rendered due to their size.

Constructs a simp context from the simp argument syntax.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Meta.NormNum.elabNormNum (args : Lean.Syntax) (loc : Lean.Syntax) (simpOnly : ) (useSimp : ) :

Elaborates a call to norm_num only? [args] or norm_num1.

• args: the (simpArgs)? syntax for simp arguments
• loc: the (location)? syntax for the optional location argument
• simpOnly: true if only was used in norm_num
• useSimp: false if norm_num1 was used, in which case only the structural parts of simp will be used, not any of the post-processing that simp only does without lemmas
Equations
• One or more equations did not get rendered due to their size.

Normalize numerical expressions. Supports the operations + - * / ⁻¹⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B≠ B, A < B and A ≤ B≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

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

Basic version of norm_num that does not call simp.

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

Basic version of norm_num that does not call simp.

Equations

Elaborator for norm_num1 conv tactic.

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

Normalize numerical expressions. Supports the operations + - * / ⁻¹⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B≠ B, A < B and A ≤ B≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

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

Elaborator for norm_num conv tactic.

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

The basic usage is #norm_num e, where e is an expression, which will print the norm_num form of e.

Syntax: #norm_num (only)? ([ simp lemma list ])? :? expression

This accepts the same options as the #simp command. You can specify additional simp lemmas as usual, for example using #norm_num [f, g] : e. (The colon is optional but helpful for the parser.) The only restricts norm_num to using only the provided lemmas, and so #norm_num only : e behaves similarly to norm_num1.

Unlike norm_num, this command does not fail when no simplifications are made.

#norm_num` understands local variables, so you can use them to introduce parameters.

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