Add test

rems-project · Feb 13, 2025 · bbad0f3 · bbad0f3
1 parent dc3751e
commit bbad0f3
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
@@ -12,6 +12,13 @@ def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
 def foo (x : (BitVec 8)) : (BitVec 16) :=
   (EXTZ x)
 
+/-- Type quantifiers: k_ex868# : Bool, n : Nat, n ≥ 0 -/
+def slice_mask2 {n : _} (i : (BitVec n)) (l : (BitVec n)) (b : Bool) : (BitVec n) :=
+  if b
+  then i
+  else let one : (BitVec n) := (EXTZ l)
+       (HAdd.hAdd one one)
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
diff --git a/test/lean/implicit.sail b/test/lean/implicit.sail
@@ -9,3 +9,12 @@ val foo : bits(8) -> bits(16)
 function foo x = {
   EXTZ(x)
 }
+
+val slice_mask2 : forall 'n, 'n >= 0. (implicit('n), bits('n), bits('n), bool) -> bits('n)
+function slice_mask2(n,i,l,b) =
+  if b then {
+    i
+  } else {
+    let one : bits('n) = EXTZ(n, l) in
+    one + one
+  }