summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean15
1 files changed, 15 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 6e7733a7..9e65d3c0 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -764,6 +764,21 @@ def U32.ofInt := @Scalar.ofInt .U32
def U64.ofInt := @Scalar.ofInt .U64
def U128.ofInt := @Scalar.ofInt .U128
+postfix:74 "%isize" => Isize.ofInt
+postfix:74 "%i8" => I8.ofInt
+postfix:74 "%i16" => I16.ofInt
+postfix:74 "%i32" => I32.ofInt
+postfix:74 "%i64" => I64.ofInt
+postfix:74 "%i128" => I128.ofInt
+postfix:74 "%usize" => Usize.ofInt
+postfix:74 "%u8" => U8.ofInt
+postfix:74 "%u16" => U16.ofInt
+postfix:74 "%u32" => U32.ofInt
+postfix:74 "%u64" => U64.ofInt
+postfix:74 "%u128" => U128.ofInt
+
+example : Result U32 := 1%u32 + 2%u32
+
-- TODO: factor those lemmas out
@[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
simp [Scalar.ofInt, Scalar.ofIntCore]