test: toExpr tests

Motivation: consistency with `mkRawNatLit`

src/Init/Data/BitVec/Basic.lean

@@ -8,8 +8,6 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 
-namespace Std
-
 /-!
 We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
 (Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
@@ -35,6 +33,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
+@[deprecated] abbrev Std.BitVec := _root_.BitVec
+
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
@@ -166,7 +166,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -606,3 +606,5 @@ section normalization_eqs
 @[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
+
+end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -45,7 +45,7 @@ end Bool
 
 /-! ### Preliminaries -/
 
-namespace Std.BitVec
+namespace BitVec
 
 private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
@@ -173,3 +173,5 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 /-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
+
+end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -8,7 +8,7 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,3 +57,5 @@ theorem iunfoldr_replace
     (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
+
+end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -598,3 +598,5 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   let ⟨y, lt⟩ := y
   simp
   exact Nat.lt_of_le_of_ne
+
+end BitVec

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Omega.LinearCombo
 import Init.Omega.Int
 import Init.Omega.Logic
+import Init.Data.BitVec
 import Lean.Meta.AppBuilder
 
 /-!
@@ -173,8 +174,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
-      | _, (`Std.BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const `Std.BitVec.toNat_lt []) n x)
+      | _, (``BitVec.toNat, #[n, x]) =>
+        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with

src/Lean/Expr.lean

@@ -912,7 +912,7 @@ def litValue! : Expr → Literal
   | lit v => v
   | _     => panic! "literal expected"
 
-def isNatLit : Expr → Bool
+def isRawNatLit : Expr → Bool
   | lit (Literal.natVal _) => true
   | _                      => false
 
@@ -925,7 +925,7 @@ def isStringLit : Expr → Bool
   | _                      => false
 
 def isCharLit : Expr → Bool
-  | app (const c _) a => c == ``Char.ofNat && a.isNatLit
+  | app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
   | _                 => false
 
 def constName! : Expr → Name

src/Lean/Meta/DiscrTree.lean

@@ -172,7 +172,7 @@ private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Arr
   - `Nat.succ x` where `isNumeral x`
   - `OfNat.ofNat _ x _` where `isNumeral x` -/
 private partial def isNumeral (e : Expr) : Bool :=
-  if e.isNatLit then true
+  if e.isRawNatLit then true
   else
     let f := e.getAppFn
     if !f.isConst then false

src/Lean/Meta/Match/Match.lean

@@ -96,7 +96,7 @@ private def hasValPattern (p : Problem) : Bool :=
 
 private def hasNatValPattern (p : Problem) : Bool :=
   p.alts.any fun alt => match alt.patterns with
-    | .val v :: _ => v.isNatLit
+    | .val v :: _ => v.isRawNatLit -- TODO: support `OfNat.ofNat`?
     | _           => false
 
 private def hasVarPattern (p : Problem) : Bool :=

src/Lean/Meta/Match/MatchEqs.lean

@@ -356,7 +356,7 @@ private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
         unless (← isDefEq lhs rhs) do
           let lhs ← whnf lhs
           let rhs ← whnf rhs
-          unless lhs.isNatLit && rhs.isNatLit do
+          unless lhs.isRawNatLit && rhs.isRawNatLit do
             try
               match (← injection mvarId localDecl.fvarId) with
               | InjectionResult.solved  => return InjectionAnyResult.solved

src/Lean/Meta/Match/Value.lean

@@ -16,7 +16,7 @@ private def isUIntTypeName (n : Name) : Bool :=
   UIntTypeNames.contains n
 
 def isFinPatLit (e : Expr) : Bool :=
-  e.isAppOfArity `Fin.ofNat 2 && e.appArg!.isNatLit
+  e.isAppOfArity `Fin.ofNat 2 && e.appArg!.isRawNatLit
 
 /-- Return `some (typeName, numLit)` if `v` is of the form `UInt*.mk (Fin.ofNat _ numLit)` -/
 def isUIntPatLit? (v : Expr) : Option (Name × Expr) :=
@@ -43,6 +43,6 @@ def foldPatValue (v : Expr) : Expr :=
 
 /-- Return true is `e` is a term that should be processed by the `match`-compiler using `casesValues` -/
 def isMatchValue (e : Expr) : Bool :=
-  e.isNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
+  e.isRawNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
 
 end Lean.Meta

src/Lean/Meta/Reduce.lean

@@ -32,7 +32,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
                 args ← args.modifyM i visit
             else
               args ← args.modifyM i visit
-          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isNatLit then
+          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then
             return mkRawNatLit (args[0]!.natLit?.get! + 1)
           else
             return mkAppN f args

src/Lean/Meta/Tactic/Injection.lean

@@ -111,7 +111,7 @@ where
       if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
         let lhs ← whnf lhs
         let rhs ← whnf rhs
-        if lhs.isNatLit && rhs.isNatLit then cont
+        if lhs.isRawNatLit && rhs.isRawNatLit then cont
         else
           try
             match (← injection mvarId fvarId newNames) with

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -8,7 +8,7 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
 
-namespace Std.BitVec
+namespace BitVec
 open Lean Meta Simp
 
 /-- A bit-vector literal -/
@@ -30,16 +30,16 @@ private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+Try to convert an `BitVec.ofNat`-application into a bitvector literal.
 -/
 private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  guard (e.isAppOfArity ``BitVec.ofNat 2)
   let n ← Nat.fromExpr? e.appFn!.appArg!
   let v ← Nat.fromExpr? e.appArg!
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
+Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
 def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
@@ -48,9 +48,9 @@ def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
 /--
 Convert a bitvector literal into an expression.
 -/
--- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+-- Using `BitVec.ofNat` because it is being used in `simp` theorems
 def Literal.toExpr (lit : Literal) : Expr :=
-  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -305,4 +305,4 @@ builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   let lit : Literal := { n, value := allOnes n }
   return .done { expr := lit.toExpr }
 
-end Std.BitVec
+end BitVec

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -33,7 +33,7 @@ def Config.updateArith (c : Config) : CoreM Config := do
 
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
-  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isNatLit
+  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit
 
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -288,7 +288,7 @@ where
 partial def isTrivialBottomUp (e : Expr) : AnalyzeM Bool := do
   let opts ← getOptions
   return e.isFVar
-         || e.isConst || e.isMVar || e.isNatLit || e.isStringLit || e.isSort
+         || e.isConst || e.isMVar || e.isRawNatLit || e.isStringLit || e.isSort
          || (getPPAnalyzeTrustOfNat opts && e.isAppOfArity ``OfNat.ofNat 3)
          || (getPPAnalyzeTrustOfScientific opts && e.isAppOfArity ``OfScientific.ofScientific 5)
 

src/Lean/ToExpr.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Expr
+import Init.Data.BitVec.Basic
 universe u
 
 namespace Lean
@@ -42,6 +43,53 @@ where
     mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r
         (.app (.const ``instOfNat []) r)
 
+instance : ToExpr (Fin n) where
+  toTypeExpr := .app (mkConst ``Fin) (toExpr n)
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
+      (mkApp2 (.const ``Fin.instOfNat []) (mkRawNatLit (n-1)) r)
+
+instance : ToExpr (BitVec n) where
+  toTypeExpr := .app (mkConst ``BitVec) (toExpr n)
+  -- Remark: We use ``BitVec.ofNat to represent bitvector literals
+  toExpr a := mkApp2 (.const ``BitVec.ofNat []) (toExpr n) (toExpr a.toNat)
+
+instance : ToExpr UInt8 where
+  toTypeExpr := mkConst ``UInt8
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
+      (.app (.const ``UInt8.instOfNat []) r)
+
+instance : ToExpr UInt16 where
+  toTypeExpr := mkConst ``UInt16
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
+      (.app (.const ``UInt16.instOfNat []) r)
+
+instance : ToExpr UInt32 where
+  toTypeExpr := mkConst ``UInt32
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
+      (.app (.const ``UInt32.instOfNat []) r)
+
+instance : ToExpr UInt64 where
+  toTypeExpr := mkConst ``UInt64
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
+      (.app (.const ``UInt64.instOfNat []) r)
+
+instance : ToExpr USize where
+  toTypeExpr := mkConst ``USize
+  toExpr a :=
+    let r := mkRawNatLit a.val
+    mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
+      (.app (.const ``USize.instOfNat []) r)
+
 instance : ToExpr Bool where
   toExpr     := fun b => if b then mkConst ``Bool.true else mkConst ``Bool.false
   toTypeExpr := mkConst ``Bool

tests/lean/binop_at_pattern_issue.lean

@@ -1,5 +1,5 @@
-open Std BitVec
-def f4 (v : Std.BitVec 32) : Nat :=
+open BitVec
+def f4 (v : BitVec 32) : Nat :=
   match v with
   | 10#20 ++ 0#12  => 0 -- Should be rejected since `++` does not have `[match_pattern]`
   | _ => 1

tests/lean/run/bitvec_fin_literal_norm.lean

@@ -1,4 +1,4 @@
-open Std BitVec
+open BitVec
 
 example : (5 : Fin 4) = x := by
   simp

tests/lean/run/bitvec_simproc.lean

@@ -3,45 +3,45 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-open Std BitVec
+open BitVec
 
-example (h : x = (6 : Std.BitVec 3)) : x = -2 := by
+example (h : x = (6 : BitVec 3)) : x = -2 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = ~~~2 := by
+example (h : x = (5 : BitVec 3)) : x = ~~~2 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.abs (-1#32) := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.abs (-1#32) := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = 2 + 3 := by
+example (h : x = (5 : BitVec 3)) : x = 2 + 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = 5 &&& 3 := by
+example (h : x = (1 : BitVec 3)) : x = 5 &&& 3 := by
   simp; guard_target =ₛ x = 1#3; assumption
-example (h : x = (7 : Std.BitVec 3)) : x = 5 ||| 3 := by
+example (h : x = (7 : BitVec 3)) : x = 5 ||| 3 := by
   simp; guard_target =ₛ x = 7#3; assumption
-example (h : x = (6 : Std.BitVec 3)) : x = 5 ^^^ 3 := by
+example (h : x = (6 : BitVec 3)) : x = 5 ^^^ 3 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (3 : Std.BitVec 32)) : x = 5 - 2 := by
+example (h : x = (3 : BitVec 32)) : x = 5 - 2 := by
   simp; guard_target =ₛ x = 3#32; assumption
-example (h : x = (10 : Std.BitVec 32)) : x = 5 * 2 := by
+example (h : x = (10 : BitVec 32)) : x = 5 * 2 := by
   simp; guard_target =ₛ x = 10#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = 9 / 2 := by
+example (h : x = (4 : BitVec 32)) : x = 9 / 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 9 % 2 := by
+example (h : x = (1 : BitVec 32)) : x = 9 % 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = udiv 9 2 := by
+example (h : x = (4 : BitVec 32)) : x = udiv 9 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = umod 9 2 := by
+example (h : x = (1 : BitVec 32)) : x = umod 9 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = sdiv (-9) (-2) := by
+example (h : x = (4 : BitVec 32)) : x = sdiv (-9) (-2) := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smod (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = smod (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtUDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtUDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - srem (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = - srem (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtSDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtSDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smtSDiv (-9) 0 := by
+example (h : x = (1 : BitVec 32)) : x = smtSDiv (-9) 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
 example (h : x = false) : x = (4#3).getLsb 0:= by
   simp; guard_target =ₛ x = false; assumption
@@ -51,29 +51,29 @@ example (h : x = true) : x = (4#3).getMsb 0:= by
   simp; guard_target =ₛ x = true; assumption
 example (h : x = false) : x = (4#3).getMsb 2:= by
   simp; guard_target =ₛ x = false; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = 6#32 <<< 2 := by
+example (h : x = (24 : BitVec 32)) : x = 6#32 <<< 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 6#32 >>> 2 := by
+example (h : x = (1 : BitVec 32)) : x = 6#32 >>> 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
+example (h : x = (24 : BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (2 : Std.BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
+example (h : x = (2 : BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
   simp; guard_target =ₛ x = 2#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
+example (h : x = (5 : BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (3 : Std.BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
+example (h : x = (3 : BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
   simp; guard_target =ₛ x = 3#3; assumption
-example (h : x = (7 : Std.BitVec 5)) : x = 1#3 ++ 3#2 := by
+example (h : x = (7 : BitVec 5)) : x = 1#3 ++ 3#2 := by
   simp; guard_target =ₛ x = 7#5; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
+example (h : x = (1 : BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x = 5) : x = (2#3 + 3#3).toNat := by
   simp; guard_target =ₛ x = 5; assumption
 example (h : x = -1) : x = (2#3 - 3#3).toInt := by
   simp; guard_target =ₛ x = -1; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
+example (h : x = (1 : BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x) : x = (1#3 < 3#3) := by
   simp; guard_target =ₛ x; assumption
@@ -99,15 +99,15 @@ example (h : x) : x = (3#3 ≥ 1#3) := by
   simp; guard_target =ₛ x; assumption
 example (h : ¬x) : x = (3#3 ≥ 4#3) := by
   simp; guard_target =ₛ ¬x; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
   simp; guard_target =ₛ x = 5#7; assumption
-example (h : x = (80 : Std.BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
+example (h : x = (80 : BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
   simp; guard_target =ₛ x = 80#7; assumption
-example (h : x = (5: Std.BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
+example (h : x = (5: BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (9: Std.BitVec 6)) : x = (1#3).replicate 2 := by
+example (h : x = (9: BitVec 6)) : x = (1#3).replicate 2 := by
   simp; guard_target =ₛ x = 9#6; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend 7 := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend 7 := by
   simp; guard_target =ₛ x = 5#7; assumption
 example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ1019#10 = x; assumption

tests/lean/run/omega.lean

@@ -1,4 +1,3 @@
-
 example : True := by
   fail_if_success omega
   trivial
@@ -428,7 +427,7 @@ example : 2^7 < 165 := by omega
 example (_ : x % 2^7 < 3) : x % 128 < 5 := by omega
 
 /-! ### BitVec -/
-open Std BitVec
+open BitVec
 
 example (x y : BitVec 8) (_ : x < y) : x ≠ y := by
   bv_omega

tests/lean/toExpr.lean

@@ -0,0 +1,21 @@
+import Lean
+
+open Lean BitVec
+
+open Meta in
+def test [ToExpr α] (a : α) : MetaM Unit := do
+  let e := toExpr a
+  let type ← inferType e
+  check e
+  logInfo m!"{e} : {type}"
+
+run_meta test (2 : Fin 4)
+run_meta test (8 : Fin 5)
+run_meta test (300#8)
+run_meta test (300#32)
+run_meta test (58#8)
+run_meta test (20 : UInt8)
+run_meta test (30 : UInt16)
+run_meta test (40 : UInt32)
+run_meta test (50 : UInt64)
+run_meta test (60 : USize)

tests/lean/toExpr.lean.expected.out

@@ -0,0 +1,10 @@
+2 : Fin 4
+3 : Fin 5
+44#8 : BitVec 8
+300#32 : BitVec 32
+58#8 : BitVec 8
+20 : UInt8
+30 : UInt16
+40 : UInt32
+50 : UInt64
+60 : USize