File tree Expand file tree Collapse file tree 2 files changed +1
-7
lines changed Expand file tree Collapse file tree 2 files changed +1
-7
lines changed Original file line number Diff line number Diff line change @@ -12,12 +12,6 @@ namespace String
12
12
lemma congr_append : ∀ (a b : String), a ++ b = String.mk (a.data ++ b.data)
13
13
| ⟨_⟩, ⟨_⟩ => rfl
14
14
15
- @[simp] lemma length_append : ∀ (as bs : String), (as ++ bs).length = as.length + bs.length
16
- | ⟨as⟩, ⟨bs⟩ => by
17
- rw [congr_append]
18
- simp only [String.length]
19
- exact List.length_append as bs
20
-
21
15
@[simp] lemma length_replicate (n : ℕ) (c : Char) : (replicate n c).length = n := by
22
16
simp only [String.length, String.replicate, List.length_replicate]
23
17
Original file line number Diff line number Diff line change 4
4
[{"url" : " https://github.com/leanprover/std4" ,
5
5
"type" : " git" ,
6
6
"subDir" : null ,
7
- "rev" : " cb172855f1712a9e906e91f3e14541960562fb78 " ,
7
+ "rev" : " e840c18f7334c751efbd4cfe531476e10c943cdb " ,
8
8
"name" : " std" ,
9
9
"manifestFile" : " lake-manifest.json" ,
10
10
"inputRev" : " main" ,
You can’t perform that action at this time.
0 commit comments