feat: make `<num>#<term>` bitvector literal notation global

[leodemoura]

The bitvector literal notation (e.g., 0x1#4) is currently scoped, but it is used when pretty-printing. This has led to confusion among users who find that the notation does not work in their code unless they include open BitVec.

Users are often puzzled when they try to use the bitvector literal notation directly in their code, only to find it doesn't work without explicitly opening BitVec. This behavior seems counterintuitive and has been a source of frustration. Additionally, this notation is popular among users for its compact and expressive representation.

• Alternative Notations:
  • Using polymorphic numerals (e.g., 1) loses valuable bitvector size information.
  • Using the verbose form (e.g., (1 : BitVec 4)) is cumbersome and less readable.

@kmill and @semorrison suggested the updated syntax definition for bitvector literals:

scoped syntax:max num noWs "#" noWs term:max : term
macro_rules | `($i:num#$n) => `(BitVec.ofNat $n $i)

This change ensures that:

• There is no lexical conflict with existing Mathlib notations, particularly with cardinality and Finset notations.

• The notation remains intuitive and easy to use.

• Users will no longer need to remember to open BitVec to use the notation, making it more intuitive and less error-prone.

• Pretty-printing BitVec-heavy goals, such as those in the SSFT24 tutorial, will be more readable and less verbose.

• We can still write 0#n to denote BitVec.ofNat n 0