From bbad0f32c81eadcb0bca9da1ba8c8948b5638519 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Thu, 13 Feb 2025 16:34:07 +0000
Subject: [PATCH] Add test

---
 test/lean/implicit.expected.lean | 7 +++++++
 test/lean/implicit.sail          | 9 +++++++++
 2 files changed, 16 insertions(+)

diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
index 4f6c21a58..3f01a4588 100644
--- 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
index 161f88392..605a65c3f 100644
--- 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
+  }