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)