feat: Bool.to(U)IntX

src/Init/Data/SInt/Basic.lean

@@ -148,6 +148,9 @@ instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
 instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
 instance : DecidableEq Int8 := Int8.decEq
 
+@[extern "lean_bool_to_int8"]
+def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
+
 @[extern "lean_int8_dec_lt"]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -249,6 +252,9 @@ instance : ShiftLeft Int16   := ⟨Int16.shiftLeft⟩
 instance : ShiftRight Int16  := ⟨Int16.shiftRight⟩
 instance : DecidableEq Int16 := Int16.decEq
 
+@[extern "lean_bool_to_int16"]
+def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
+
 @[extern "lean_int16_dec_lt"]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -354,6 +360,9 @@ instance : ShiftLeft Int32   := ⟨Int32.shiftLeft⟩
 instance : ShiftRight Int32  := ⟨Int32.shiftRight⟩
 instance : DecidableEq Int32 := Int32.decEq
 
+@[extern "lean_bool_to_int32"]
+def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
+
 @[extern "lean_int32_dec_lt"]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -463,6 +472,9 @@ instance : ShiftLeft Int64   := ⟨Int64.shiftLeft⟩
 instance : ShiftRight Int64  := ⟨Int64.shiftRight⟩
 instance : DecidableEq Int64 := Int64.decEq
 
+@[extern "lean_bool_to_int64"]
+def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
+
 @[extern "lean_int64_dec_lt"]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -574,6 +586,9 @@ instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
 instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
 instance : DecidableEq ISize := ISize.decEq
 
+@[extern "lean_bool_to_isize"]
+def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
+
 @[extern "lean_isize_dec_lt"]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))

src/Init/Data/UInt/Basic.lean

@@ -56,6 +56,9 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
+@[extern "lean_bool_to_uint8"]
+def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
+
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@@ -116,6 +119,9 @@ instance : Xor UInt16       := ⟨UInt16.xor⟩
 instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
+@[extern "lean_bool_to_uint16"]
+def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
+
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
@@ -174,6 +180,9 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
+@[extern "lean_bool_to_uint32"]
+def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
+
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
@@ -278,5 +287,8 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
+@[extern "lean_bool_to_usize"]
+def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
+
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/include/lean/lean.h

@@ -1617,7 +1617,16 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
 
 /* Bool */
 
-static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
+static inline uint8_t lean_bool_to_uint8(uint8_t a) { return a; }
+static inline uint16_t lean_bool_to_uint16(uint8_t a) { return (uint16_t)a; }
+static inline uint32_t lean_bool_to_uint32(uint8_t a) { return (uint32_t)a; }
+static inline uint64_t lean_bool_to_uint64(uint8_t a) { return (uint64_t)a; }
+static inline size_t lean_bool_to_usize(uint8_t a) { return (size_t)a; }
+static inline uint8_t lean_bool_to_int8(uint8_t a) { return (uint8_t)(int8_t)a; }
+static inline uint16_t lean_bool_to_int16(uint8_t a) { return (uint16_t)(int16_t)a; }
+static inline uint32_t lean_bool_to_int32(uint8_t a) { return (uint32_t)(int32_t)a; }
+static inline uint64_t lean_bool_to_int64(uint8_t a) { return (uint64_t)(int64_t)a; }
+static inline size_t lean_bool_to_isize(uint8_t a) { return (size_t)(ptrdiff_t)a; }
 
 
 /* UInt8 */

tests/lean/bool2int.lean

@@ -0,0 +1,20 @@
+#eval Bool.toUInt8 false = 0
+#eval Bool.toUInt8 true = 1
+#eval Bool.toUInt16 false = 0
+#eval Bool.toUInt16 true = 1
+#eval Bool.toUInt32 false = 0
+#eval Bool.toUInt32 true = 1
+#eval Bool.toUInt64 false = 0
+#eval Bool.toUInt64 true = 1
+#eval Bool.toUSize false = 0
+#eval Bool.toUSize true = 1
+#eval Bool.toInt8 false = 0
+#eval Bool.toInt8 true = 1
+#eval Bool.toInt16 false = 0
+#eval Bool.toInt16 true = 1
+#eval Bool.toInt32 false = 0
+#eval Bool.toInt32 true = 1
+#eval Bool.toInt64 false = 0
+#eval Bool.toInt64 true = 1
+#eval Bool.toISize false = 0
+#eval Bool.toISize true = 1

tests/lean/bool2int.lean.expected.out

@@ -0,0 +1,20 @@
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true
+true