norm_num
basic plugins #
This file adds norm_num
plugins for
- constructors and constants
Nat.cast
,Int.cast
, andmkRat
+
,-
,*
, and/
Nat.succ
,Nat.sub
,Nat.mod
, andNat.div
.
See other files in this directory for many more plugins.
Constructors and constants #
The norm_num
extension which identifies an expression OfNat.ofNat n
, returning n
.
Instances For
The norm_num
extension which identifies the expression Int.natAbs n
such that
norm_num
successfully recognizes n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Casts #
Alias of Mathlib.Meta.NormNum.isNat_natCast
.
Alias of Mathlib.Meta.NormNum.isNat_intCast
.
Alias of Mathlib.Meta.NormNum.isintCast
.
Arithmetic #
If b
divides a
and a
is invertible, then b
is invertible.
Equations
- Mathlib.Meta.NormNum.invertibleOfMul k b (↑k * b) ⋯ = { invOf := c * ↑k, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
Instances For
If b
divides a
and a
is invertible, then b
is invertible.
Equations
Instances For
Consider an Option
as an object in the MetaM
monad, by throwing an error on none
.
Equations
Instances For
Main part of evalAdd
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Main part of evalNeg
.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Meta.NormNum.evalNeg.core e f a (Mathlib.Meta.NormNum.Result'.isBool val proof) rα = failure
Instances For
Main part of evalAdd
.
Instances For
Main part of evalMul
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Helper function to synthesize a typed DivisionRing α
expression.
Equations
- Mathlib.Meta.NormNum.inferDivisionRing α = do let __do_lift ← Qq.synthInstanceQ q(DivisionRing «$α») <|> Lean.throwError (Lean.toMessageData "not a division ring") pure __do_lift