chore: add match_pattern attribute for Std.BitVec.ofNat (#320)

leanprover-community · Oct 24, 2023 · ab21923 · ab21923
1 parent fb56324
commit ab21923
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Std/Data/BitVec/Basic.lean b/Std/Data/BitVec/Basic.lean
@@ -80,6 +80,9 @@ instance : OfNat (BitVec n) i where ofNat := .ofNat n i
 scoped syntax:max term:max noWs "#" noWs term:max : term
 macro_rules | `($i#$n) => `(BitVec.ofNat $n $i)
 
+/- Support for `i#n` notation in patterns.  -/
+attribute [match_pattern] BitVec.ofNat
+
 /-- Unexpander for bit vector literals. -/
 @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
   | `($(_) $n $i) => `($i#$n)