Documentation

Std.Data.UInt

UInt8 #

theorem UInt8.ext {x : UInt8} {y : UInt8} :
@[simp]
theorem UInt8.val_val_eq_toNat (x : UInt8) :
x.val.val = UInt8.toNat x

UInt16 #

theorem UInt16.ext {x : UInt16} {y : UInt16} :
@[simp]
theorem UInt16.val_val_eq_toNat (x : UInt16) :
x.val.val = UInt16.toNat x

UInt32 #

theorem UInt32.ext {x : UInt32} {y : UInt32} :
@[simp]
theorem UInt32.val_val_eq_toNat (x : UInt32) :
x.val.val = UInt32.toNat x

UInt64 #

theorem UInt64.ext {x : UInt64} {y : UInt64} :
@[simp]
theorem UInt64.val_val_eq_toNat (x : UInt64) :
x.val.val = UInt64.toNat x

USize #

theorem USize.ext {x : USize} {y : USize} :
@[simp]
theorem USize.val_val_eq_toNat (x : USize) :
x.val.val = USize.toNat x