summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon HO2024-05-21 11:01:13 +0200
committerGitHub2024-05-21 11:01:13 +0200
commite07af56862e92efecb09209874ad24da77c0e001 (patch)
tree0c98db6c77e8c53b7e2c117aba6407beb053f36e /backends/lean/Base/Primitives
parentdc8ceedffa0945b84f81e318fa78f1e55b1731d2 (diff)
parentd088e1adbfb20d6f3137b236f750b0ac5fed4f95 (diff)
Merge pull request #183 from RaitoBezarius/coercions
feat(backends/lean): make `max`-related coercions nicer
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean12
1 files changed, 12 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index dccbcdf2..f08b8dec 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1419,6 +1419,18 @@ instance (ty: ScalarTy) : LinearOrder (Scalar ty) where
right; exact (Scalar.le_equiv _ _).2 H
decidableLE := ScalarDecidableLE ty
+-- Coercion theorems
+-- This is helpful whenever you want to "push" casts to the innermost nodes
+-- and make the cast normalization happen more magically.
+
+@[simp, norm_cast]
+theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (↑a) (↑b): ℤ) := by
+ -- TODO: there should be a shorter way to prove this.
+ rw [max_def, max_def]
+ split_ifs <;> simp_all
+ refine' absurd _ (lt_irrefl a)
+ exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption))
+
-- Leading zeros
def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry
def core.num.U8.leading_zeros (x : U8) : U32 := sorry