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

chore: parameter naming convention

Browse source
This commit is contained in:
Leonardo de Moura 2021-06-06 17:09:02 -07:00
parent 9200de01ef
commit e8a958d8f3
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Data/String/Basic.lean
View file

@ -268,8 +268,8 @@ def offsetOfPos (s : String) (pos : Pos) : Nat :=
else loop (s.next i) (f a (s.get i))
loop i a
@[inline] def foldl {α : Type u} (f : α → Char → α) (a : α) (s : String) : α :=
foldlAux f s s.bsize 0 a
@[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
foldlAux f s s.bsize 0 init
@[specialize] partial def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : Pos) (i : Pos) : α :=
let rec loop (i : Pos) :=
@ -277,8 +277,8 @@ def offsetOfPos (s : String) (pos : Pos) : Nat :=
else f (s.get i) (loop (s.next i))
loop i
@[inline] def foldr {α : Type u} (f : Char → α → α) (a : α) (s : String) : α :=
foldrAux f a s s.bsize 0
@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
foldrAux f init s s.bsize 0
@[specialize] partial def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool :=
let rec loop (i : Pos) :=
@ -415,13 +415,13 @@ partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
loop b (s.next i) 0 r
loop s.startPos s.startPos 0 []
@[inline] def foldl {α : Type u} (f : α → Char → α) (a : α) (s : Substring) : α :=
@[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α :=
match s with
| ⟨s, b, e⟩ => String.foldlAux f s e b a
| ⟨s, b, e⟩ => String.foldlAux f s e b init
@[inline] def foldr {α : Type u} (f : Char → α → α) (a : α) (s : Substring) : α :=
@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring) : α :=
match s with
| ⟨s, b, e⟩ => String.foldrAux f a s e b
| ⟨s, b, e⟩ => String.foldrAux f init s e b
@[inline] def any (s : Substring) (p : Char → Bool) : Bool :=
match s with