From 8896c9b06d5ec2d66400f733b6ec4066ec932b85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Jan 2022 18:47:03 -0800 Subject: [PATCH] test: add variant of `Formula.count_quantifiers` see #974 --- tests/lean/974.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/lean/974.lean b/tests/lean/974.lean index 45a00cd0b0..195fb2bf85 100644 --- a/tests/lean/974.lean +++ b/tests/lean/974.lean @@ -13,3 +13,8 @@ attribute [simp] Formula.count_quantifiers #check @Formula.count_quantifiers._eq_1 #check @Formula.count_quantifiers._eq_2 #check @Formula.count_quantifiers._eq_3 + +@[simp] def Formula.count_quantifiers2 : Formula n → Nat +| imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2 +| all f => f.count_quantifiers2 + 1 +| _ => 0