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

chore: remove intermediate

Browse source
This commit is contained in:
Mario Carneiro 2023-05-17 04:40:57 -04:00 • committed by Leonardo de Moura
parent 2ae78f3c45
commit bc841809c2
1 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -398,21 +398,19 @@ termination_by _ => i.1
foldrAux f init s s.endPos 0
@[specialize] def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool :=
let rec loop (i : Pos) :=
if h : i < stopPos then
if p (s.get i) then true
else
have := Nat.sub_lt_sub_left h (lt_next s i)
loop (s.next i)
else false
loop i
termination_by loop => stopPos.1 - i.1
if h : i < stopPos then
if p (s.get i) then true
else
have := Nat.sub_lt_sub_left h (lt_next s i)
anyAux s stopPos p (s.next i)
else false
termination_by _ => stopPos.1 - i.1
@[inline] def any (s : String) (p : Char → Bool) : Bool :=
anyAux s s.endPos p 0
anyAux s s.endPos p 0
@[inline] def all (s : String) (p : Char → Bool) : Bool :=
!s.any (fun c => !p c)
!s.any (fun c => !p c)
def contains (s : String) (c : Char) : Bool :=
s.any (fun a => a == c)