diff options
| author | Son HO | 2024-04-15 20:01:59 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-15 20:01:59 +0200 |
| commit | 23da71768c03d955c916635bfc5c9d5806a80187 (patch) | |
| tree | 818252b795167a9a6ee366c85e901273d38b8374 /backends/lean/Base/Primitives | |
| parent | 2545ad25384156d7d8d798567bc922be798a20e3 (diff) | |
| parent | c1c33de85906bda71cac098ddba0e5dfc98c85d2 (diff) | |
Merge pull request #126 from RaitoBezarius/scalar-preorders
lean: scalars form a preorder
Diffstat (limited to 'backends/lean/Base/Primitives')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index b8d93d30..be930754 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1394,6 +1394,16 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by simp [eq_equiv] +instance (ty: ScalarTy) : Preorder (Scalar ty) where + le_refl := fun a => by simp + le_trans := fun a b c => by + intro Hab Hbc + exact (le_trans ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hbc)) + lt_iff_le_not_le := fun a b => by + trans (a: Int) < (b: Int); exact (Scalar.lt_equiv _ _) + trans (a: Int) ≤ (b: Int) ∧ ¬ (b: Int) ≤ (a: Int); exact lt_iff_le_not_le + repeat rewrite [← Scalar.le_equiv]; rfl + -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry |