chore: add test for multi arity

leanprover · Nov 22, 2024 · b59b96f · b59b96f
1 parent fc57b21
commit b59b96f
Showing 1 changed file with 16 additions and 2 deletions.
diff --git a/tests/lean/run/ackermannize.lean b/tests/lean/run/ackermannize.lean
@@ -5,8 +5,8 @@ import Lean.Elab.Tactic.BVAckermannize
 set_option trace.bv_ack true
 
 /- Test that we correctly handle arrow / forall -/
-theorem foo (f : BitVec 1 → BitVec 1) (x : BitVec 1) : 
-    ((1#1 ^^^ f x ^^^ (f (x + 1))) = 0#1) → 
+theorem foo (f : BitVec 1 → BitVec 1) (x : BitVec 1) :
+    ((1#1 ^^^ f x ^^^ (f (x + 1))) = 0#1) →
     ((f 0#1 = 1#1) ∨ (f 1#1 = 1#1)) := by
   try bv_decide
   bv_ack_eager
@@ -54,3 +54,17 @@ theorem true_on_one_input_of_neg_comm (g : BitVec 1 → BitVec 1) (x : BitVec 1)
 
 /-- info: 'true_on_one_input_of_neg_comm' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] -/
 #guard_msgs in  #print axioms true_on_one_input_of_neg_comm
+
+/- Test that multi artity functions work -/
+theorem less_6E_bin_predicate (P : BitVec 2 → BitVec 2 → Bool)
+  (x : BitVec 2) (y : BitVec 2) (hx : x ≤ 1#2) (hy : y ≤ 1#2)
+  (h : P 0#2 0#2 ∧ P 0#2 1#2 ∧ P 1#2 0#2 ∧ P 1#2 1#2) :
+  P x y := by
+  try bv_decide
+  bv_ack_eager
+  bv_decide
+
+/--
+info: 'less_6E_bin_predicate' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
+#guard_msgs in  #print axioms less_6E_bin_predicate