We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b0a80b1 commit f2f1a8dCopy full SHA for f2f1a8d
HumanEvalLean/Common/Brackets.lean
@@ -111,8 +111,6 @@ theorem maxBalance_append {l m : List Paren} :
111
def minBalance (l : List Paren) : Int :=
112
(0...=l.length).toList.map (fun k => balance (l.take k)) |>.min (by simp)
113
114
-attribute [simp] Std.Rcc.mem_toList_iff_mem Std.Rcc.mem_iff
115
-
116
@[grind! .]
117
theorem minBalance_nonpos (l : List Paren) : minBalance l ≤ 0 := by
118
rw [minBalance]
0 commit comments