max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: add variant of Formula.count_quantifiers

Browse source 
see #974
This commit is contained in:
Leonardo de Moura 2022-01-25 18:47:03 -08:00
parent 98407798af
commit 8896c9b06d
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/974.lean
View file

@ -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