diff options
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 285bc7fb..422cbc6a 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -488,6 +488,17 @@ class HNeg (α : Type u) (β : outParam (Type v)) where prefix:75 "-" => HNeg.hNeg +/- We need this, otherwise we break pattern matching like in: + + ``` + def is_minus_one (x : Int) : Bool := + match x with + | -1 => true + | _ => false + ``` +-/ +attribute [match_pattern] HNeg.hNeg + instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x @@ -1113,4 +1124,22 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := -- else -- .fail integerOverflow +-- Notation for pattern matching +-- We make the precedence looser than the negation. +notation:70 a:70 "#scalar" => Scalar.mk (a) _ _ + +example {ty} (x : Scalar ty) : ℤ := + match x with + | v#scalar => v + +example {ty} (x : Scalar ty) : Bool := + match x with + | 1#scalar => true + | _ => false + +example {ty} (x : Scalar ty) : Bool := + match x with + | -(1 : Int)#scalar => true + | _ => false + end Primitives |