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
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
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 }
theorem UInt32.pow_def (a : UInt32) (n : ) :
a ^ n = { val := a.val ^ n }
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 }
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
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
theorem UInt8.neg_def (a : UInt8) :
-a = { val := -a.val }
theorem UInt8.zsmul_def (z : ) (a : UInt8) :
z a = { val := z a.val }
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 }
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 }
theorem UInt64.mod_def (a : UInt64) (b : UInt64) :
a % b = { val := a.val % b.val }
theorem UInt64.zsmul_def (z : ) (a : UInt64) :
z a = { val := z a.val }
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
theorem USize.neg_def (a : USize) :
-a = { val := -a.val }
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 }
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
theorem UInt32.mul_def (a : UInt32) (b : UInt32) :
a * b = { val := a.val * b.val }
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
theorem UInt32.nsmul_def (n : ) (a : UInt32) :
n a = { val := n a.val }
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?

Instances For

    Is this a lowercase ASCII letter?

    Instances For

      Is this an alphabetic ASCII character?

      Instances For

        Is this an ASCII digit character?

        Instances For

          Is this an alphanumeric ASCII character?

          Instances For

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

            Instances For