Documentation

Mathlib.Data.UInt

theorem UInt8.val_eq_of_lt {a : } :
a < UInt8.size(UInt8.ofNat a).val = a
theorem UInt16.val_eq_of_lt {a : } :
a < UInt16.size(UInt16.ofNat a).val = a
theorem UInt32.val_eq_of_lt {a : } :
a < UInt32.size(UInt32.ofNat a).val = a
theorem UInt64.val_eq_of_lt {a : } :
a < UInt64.size(UInt64.ofNat a).val = a
theorem USize.val_eq_of_lt {a : } :
a < USize.size(USize.ofNat a).val = a
Equations
theorem USize.intCast_def (z : ) :
z = { val := z }
theorem UInt8.val_eq_of_eq {a : UInt8} {b : UInt8} :
a = ba.val = b.val
theorem USize.eq_of_val_eq {a : USize} {b : USize} :
a.val = b.vala = b
Equations
Equations
theorem UInt32.one_def :
1 = { val := 1 }
theorem USize.add_def (a : USize) (b : USize) :
a + b = { val := a.val + b.val }
theorem UInt64.neg_def (a : UInt64) :
-a = { val := -a.val }
theorem UInt16.intCast_def (z : ) :
z = { val := z }
Equations
Equations
theorem UInt32.pow_def (a : UInt32) (n : ) :
a ^ n = { val := a.val ^ n }
Equations
  • One or more equations did not get rendered due to their size.
Equations
theorem UInt64.natCast_def (n : ) :
n = { val := n }
theorem USize.zsmul_def (z : ) (a : USize) :
z a = { val := z a.val }
theorem UInt8.mul_def (a : UInt8) (b : UInt8) :
a * b = { val := a.val * b.val }
theorem USize.zero_def :
0 = { val := 0 }
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
theorem UInt8.intCast_def (z : ) :
z = { val := z }
theorem USize.natCast_def (n : ) :
n = { val := n }
theorem USize.pow_def (a : USize) (n : ) :
a ^ n = { val := a.val ^ n }
theorem UInt16.neg_def (a : UInt16) :
-a = { val := -a.val }
theorem UInt16.one_def :
1 = { val := 1 }
theorem UInt32.sub_def (a : UInt32) (b : UInt32) :
a - b = { val := a.val - b.val }
theorem UInt64.intCast_def (z : ) :
z = { val := z }
@[simp]
theorem USize.mk_val_eq (a : USize) :
{ val := a.val } = a
Equations
theorem UInt8.one_def :
1 = { val := 1 }
theorem UInt8.eq_of_val_eq {a : UInt8} {b : UInt8} :
a.val = b.vala = b
@[simp]
theorem UInt32.mk_val_eq (a : UInt32) :
{ val := a.val } = a
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
theorem UInt8.neg_def (a : UInt8) :
-a = { val := -a.val }
Equations
Equations
theorem UInt8.zsmul_def (z : ) (a : UInt8) :
z a = { val := z a.val }
Equations
theorem UInt32.intCast_def (z : ) :
z = { val := z }
theorem UInt8.pow_def (a : UInt8) (n : ) :
a ^ n = { val := a.val ^ n }
theorem UInt8.mod_def (a : UInt8) (b : UInt8) :
a % b = { val := a.val % b.val }
theorem UInt16.sub_def (a : UInt16) (b : UInt16) :
a - b = { val := a.val - b.val }
theorem UInt64.one_def :
1 = { val := 1 }
@[simp]
theorem UInt64.mk_val_eq (a : UInt64) :
{ val := a.val } = a
theorem USize.mul_def (a : USize) (b : USize) :
a * b = { val := a.val * b.val }
theorem UInt32.natCast_def (n : ) :
n = { val := n }
theorem USize.mod_def (a : USize) (b : USize) :
a % b = { val := a.val % b.val }
theorem UInt32.zsmul_def (z : ) (a : UInt32) :
z a = { val := z a.val }
Equations
theorem UInt16.add_def (a : UInt16) (b : UInt16) :
a + b = { val := a.val + b.val }
theorem UInt64.pow_def (a : UInt64) (n : ) :
a ^ n = { val := a.val ^ n }
theorem UInt16.mul_def (a : UInt16) (b : UInt16) :
a * b = { val := a.val * b.val }
theorem UInt8.nsmul_def (n : ) (a : UInt8) :
n a = { val := n a.val }
theorem UInt16.nsmul_def (n : ) (a : UInt16) :
n a = { val := n a.val }
Equations
theorem UInt64.mod_def (a : UInt64) (b : UInt64) :
a % b = { val := a.val % b.val }
Equations
theorem UInt64.zsmul_def (z : ) (a : UInt64) :
z a = { val := z a.val }
Equations
theorem UInt64.sub_def (a : UInt64) (b : UInt64) :
a - b = { val := a.val - b.val }
theorem UInt32.val_eq_of_eq {a : UInt32} {b : UInt32} :
a = ba.val = b.val
@[simp]
theorem UInt8.mk_val_eq (a : UInt8) :
{ val := a.val } = a
theorem UInt8.sub_def (a : UInt8) (b : UInt8) :
a - b = { val := a.val - b.val }
theorem USize.nsmul_def (n : ) (a : USize) :
n a = { val := n a.val }
@[simp]
theorem UInt16.mk_val_eq (a : UInt16) :
{ val := a.val } = a
Equations
  • One or more equations did not get rendered due to their size.
Equations
theorem USize.neg_def (a : USize) :
-a = { val := -a.val }
Equations
theorem UInt64.nsmul_def (n : ) (a : UInt64) :
n a = { val := n a.val }
theorem UInt16.val_eq_of_eq {a : UInt16} {b : UInt16} :
a = ba.val = b.val
theorem UInt32.add_def (a : UInt32) (b : UInt32) :
a + b = { val := a.val + b.val }
theorem UInt32.eq_of_val_eq {a : UInt32} {b : UInt32} :
a.val = b.vala = b
theorem UInt32.neg_def (a : UInt32) :
-a = { val := -a.val }
Equations
Equations
theorem USize.one_def :
1 = { val := 1 }
theorem UInt64.zero_def :
0 = { val := 0 }
theorem UInt16.zero_def :
0 = { val := 0 }
theorem UInt16.natCast_def (n : ) :
n = { val := n }
theorem UInt32.mod_def (a : UInt32) (b : UInt32) :
a % b = { val := a.val % b.val }
theorem UInt64.val_eq_of_eq {a : UInt64} {b : UInt64} :
a = ba.val = b.val
theorem UInt64.mul_def (a : UInt64) (b : UInt64) :
a * b = { val := a.val * b.val }
theorem UInt32.zero_def :
0 = { val := 0 }
theorem USize.val_eq_of_eq {a : USize} {b : USize} :
a = ba.val = b.val
theorem UInt16.mod_def (a : UInt16) (b : UInt16) :
a % b = { val := a.val % b.val }
theorem UInt8.natCast_def (n : ) :
n = { val := n }
theorem UInt64.eq_of_val_eq {a : UInt64} {b : UInt64} :
a.val = b.vala = b
Equations
Equations
Equations
Equations
theorem UInt32.mul_def (a : UInt32) (b : UInt32) :
a * b = { val := a.val * b.val }
Equations
theorem USize.sub_def (a : USize) (b : USize) :
a - b = { val := a.val - b.val }
theorem UInt8.zero_def :
0 = { val := 0 }
theorem UInt16.eq_of_val_eq {a : UInt16} {b : UInt16} :
a.val = b.vala = b
Equations
theorem UInt32.nsmul_def (n : ) (a : UInt32) :
n a = { val := n a.val }
Equations
  • One or more equations did not get rendered due to their size.
Equations
theorem UInt64.add_def (a : UInt64) (b : UInt64) :
a + b = { val := a.val + b.val }
theorem UInt16.zsmul_def (z : ) (a : UInt16) :
z a = { val := z a.val }
theorem UInt16.pow_def (a : UInt16) (n : ) :
a ^ n = { val := a.val ^ n }
theorem UInt8.add_def (a : UInt8) (b : UInt8) :
a + b = { val := a.val + b.val }

Is this an uppercase ASCII letter?

Equations

Is this a lowercase ASCII letter?

Equations

Is this an alphabetic ASCII character?

Equations

Is this an ASCII digit character?

Equations

Is this an alphanumeric ASCII character?

Equations

The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.

Equations