diff options
| author | Son Ho | 2023-10-16 11:06:46 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-16 11:06:46 +0200 |
| commit | cbb2d05e0db6bedf9d6844f29ee25b95429b994c (patch) | |
| tree | 0f6727e66f1034fdac417f3d62f903efc4fee73a /backends/lean/Base/Primitives | |
| parent | 0ba1c30f735f6e1cce771800d41042e6dc15e86f (diff) | |
Improve formatting of scalars in Lean
Diffstat (limited to 'backends/lean/Base/Primitives')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 15 |
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] |