Returns true
if e
is of the form Nat
Instances For
Returns true
if e
is of the form @instHAdd Nat instAddNat
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if e
is instLENat
Instances For
Equations
- { u := u, v := v, k := k }.neg = { u := v, v := u, k := -k - 1 }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Grind.Arith.instToMessageDataCnstrExpr = { toMessageData := fun (c : Lean.Meta.Grind.Arith.Offset.Cnstr Lean.Expr) => Lean.Meta.Grind.Arith.Offset.toMessageData c }
Returns some cnstr
if e
is offset constraint.
Remark: z
is 0
numeral. It is an extra argument because we
want to be able to provide the one that has already been internalized.
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.