From cae59c6916f032da91f54ae15e35804e7c9fe220 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Apr 2022 08:23:32 -0700 Subject: [PATCH] chore: remove staging workarounds --- src/Init/Data/Nat/SOM.lean | 2 +- src/Init/Data/String/Extra.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Nat/SOM.lean b/src/Init/Data/Nat/SOM.lean index 594bf9f808..f021500d88 100644 --- a/src/Init/Data/Nat/SOM.lean +++ b/src/Init/Data/Nat/SOM.lean @@ -122,7 +122,7 @@ where theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by match p₁ with | [] => simp! - | v :: p₁ => sorry -- TODO(0) simp! [append_denote _ p₁ p₂, Nat.add_assoc] + | v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc] theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := go hugeFuel p₁ p₂ diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index d2074bc295..707337ed2d 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -61,7 +61,7 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption) theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i := - have h : i.hasNext = true := by sorry -- TODO(0) simp_arith [atEnd] at h; simp_arith [hasNext, h] + have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h] sizeOf_next_lt_of_hasNext i h macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)