summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2024-06-12 18:20:23 +0200
committerSon Ho2024-06-12 18:20:23 +0200
commitdd2b973a86680308807d7f26aff81d3310550f84 (patch)
tree45cea441e0a493b67bb33d82c083905524c923b0 /backends/lean/Base
parent8ca43c32b30c03cc3fde51736ea5884dfd1c2c50 (diff)
Revert "Update CoreConvertNum.lean"
This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/CoreConvertNum.lean44
1 files changed, 22 insertions, 22 deletions
diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index bc3db8b2..eb456a96 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -18,40 +18,40 @@ namespace num -- core.convert.num
-- Conversions
def FromUsizeBool.from (b : Bool) : Usize :=
- if b then 1usize else 0usize
+ if b then 1#usize else 0#usize
def FromU8Bool.from (b : Bool) : U8 :=
- if b then 1u8 else 0u8
+ if b then 1#u8 else 0#u8
def FromU16Bool.from (b : Bool) : U16 :=
- if b then 1u16 else 0u16
+ if b then 1#u16 else 0#u16
def FromU32Bool.from (b : Bool) : U32 :=
- if b then 1u32 else 0u32
+ if b then 1#u32 else 0#u32
def FromU64Bool.from (b : Bool) : U64 :=
- if b then 1u64 else 0u64
+ if b then 1#u64 else 0#u64
def FromU128Bool.from (b : Bool) : U128 :=
- if b then 1u128 else 0u128
+ if b then 1#u128 else 0#u128
def FromIsizeBool.from (b : Bool) : Isize :=
- if b then 1isize else 0isize
+ if b then 1#isize else 0#isize
def FromI8Bool.from (b : Bool) : I8 :=
- if b then 1i8 else 0i8
+ if b then 1#i8 else 0#i8
def FromI16Bool.from (b : Bool) : I16 :=
- if b then 1i16 else 0i16
+ if b then 1#i16 else 0#i16
def FromI32Bool.from (b : Bool) : I32 :=
- if b then 1i32 else 0i32
+ if b then 1#i32 else 0#i32
def FromI64Bool.from (b : Bool) : I64 :=
- if b then 1i64 else 0i64
+ if b then 1#i64 else 0#i64
def FromI128Bool.from (b : Bool) : I128 :=
- if b then 1i128 else 0i128
+ if b then 1#i128 else 0#i128
def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
@@ -259,18 +259,18 @@ def FromI128I128 : core.convert.From I128 I128 := {
}
-- to_le_bytes
-def core.num.U8.to_le_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_le_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_le_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_le_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_le_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
-- to_be_bytes
-def core.num.U8.to_be_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_be_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_be_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_be_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_be_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
end core.convert