test: toExpr tests

leanprover · Feb 23, 2024 · 81a57a0 · 81a57a0
1 parent feb0195
commit 81a57a0
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 0 deletions.
diff --git a/tests/lean/toExpr.lean b/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)
diff --git a/tests/lean/toExpr.lean.expected.out b/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