sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: increase test size

Browse Source
This commit is contained in:
Leonardo de Moura
2021-03-04 17:27:24 -08:00
parent db499a646f
commit b26c7087fe
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
tests/playground/nnf.lean
View File

@@ -5,7 +5,7 @@ partial def mkBigAnd (n : Nat) (p : Syntax) : MacroM Syntax :=
where
loop (low high : Nat) : MacroM Syntax := do
if low == high then
`($p[$(quote low)])
`($p[natLit! $(quote low)])
else
let mid := (low + high)/2
`($(← loop low mid) ∧ $(← loop (mid + 1) high))
@@ -17,7 +17,7 @@ partial def mkBigOrNot (n : Nat) (p : Syntax) : MacroM Syntax :=
where
loop (low high : Nat) : MacroM Syntax := do
if low == high then
`(¬ $p[$(quote low)])
`(¬ $p[natLit! $(quote low)])
else
let mid := (low + high)/2
`($(← loop low mid) ∨ $(← loop (mid + 1) high))
@@ -26,7 +26,7 @@ macro "bigOrNot! " n:num p:ident : term => mkBigOrNot n.toNat p
@[simp] axiom not_and (p q : Prop) : (¬ (p ∧ q)) = (¬ p ∨ ¬ q)
theorem ex (p : Array Prop) : (¬ bigAnd! 500 p) = bigOrNot! 500 p := by
theorem ex (p : Array Prop) : (¬ bigAnd! 2000 p) = bigOrNot! 2000 p := by
simp only [not_and]
rfl