Init.Data.String.Basic

String.set _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := s }, i, c => { data := String.utf8SetAux c s 0 i }

source

def String.modify (s : String) (i : String.Pos) (f : Char → Char) :

String

Equations

String.modify s i f = String.set s i (f (String.get s i))

source

@[extern lean_string_utf8_next]

def String.next (s : String) (p : String.Pos) :

String.Pos

Equations

String.next s p = let c := String.get s p; p + c

source

@[extern lean_string_utf8_prev]

def String.prev:

String → String.Pos → String.Pos

Equations

String.prev _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { data := s }, p => if p = 0 then 0 else String.utf8PrevAux s 0 p

source

def String.front (s : String) :

Char

Equations

String.front s = String.get s 0

source

def String.back (s : String) :

Char

Equations

String.back s = String.get s (String.prev s (String.endPos s))

source

@[extern lean_string_utf8_at_end]

def String.atEnd:

String → String.Pos → Bool

Equations

String.atEnd _fun_discr _fun_discr = match _fun_discr, _fun_discr with | s, p => decide (p.byteIdx ≥ String.utf8ByteSize s)

source

partial def String.posOfAux (s : String) (c : Char) (stopPos : String.Pos) (pos : String.Pos) :

String.Pos

source

@[inline]

def String.posOf (s : String) (c : Char) :

String.Pos

Equations

String.posOf s c = String.posOfAux s c (String.endPos s) 0

source

partial def String.revPosOfAux (s : String) (c : Char) (pos : String.Pos) :

Option String.Pos

source

def String.revPosOf (s : String) (c : Char) :

Option String.Pos

Equations

String.revPosOf s c = if (String.endPos s == 0) = true then none else String.revPosOfAux s c (String.prev s (String.endPos s))

source

partial def String.findAux (s : String) (p : Char → Bool) (stopPos : String.Pos) (pos : String.Pos) :

String.Pos

source

@[inline]

def String.find (s : String) (p : Char → Bool) :

String.Pos

Equations

String.find s p = String.findAux s p (String.endPos s) 0

source

partial def String.revFindAux (s : String) (p : Char → Bool) (pos : String.Pos) :

Option String.Pos

source

def String.revFind (s : String) (p : Char → Bool) :

Option String.Pos

Equations

String.revFind s p = if (String.endPos s == 0) = true then none else String.revFindAux s p (String.prev s (String.endPos s))

source

@[inline]

abbrev String.Pos.min (p₁ : String.Pos) (p₂ : String.Pos) :

String.Pos

Equations

String.Pos.min p₁ p₂ = { byteIdx := Nat.min p₁.byteIdx p₂.byteIdx }

source

def String.firstDiffPos (a : String) (b : String) :

String.Pos

Returns the first position where the two strings differ.

Equations

String.firstDiffPos a b = let stopPos := String.Pos.min (String.endPos a) (String.endPos b); String.firstDiffPos.loop a b stopPos 0

source

partial def String.firstDiffPos.loop (a : String) (b : String) (stopPos : String.Pos) (i : String.Pos) :

String.Pos

source

@[extern lean_string_utf8_extract]

def String.extract:

String → String.Pos → String.Pos → String

Equations

One or more equations did not get rendered due to their size.

source

def String.extract.go₁:

List Char → String.Pos → String.Pos → String.Pos → List Char

Equations

One or more equations did not get rendered due to their size.
String.extract.go₁ [] _fun_discr _fun_discr _fun_discr = []

source

def String.extract.go₂:

List Char → String.Pos → String.Pos → List Char

Equations

String.extract.go₂ [] _fun_discr _fun_discr = []
String.extract.go₂ (c :: cs) _fun_discr _fun_discr = if _fun_discr = _fun_discr then [] else c :: String.extract.go₂ cs (_fun_discr + c) _fun_discr

source

@[specialize]

partial def String.splitAux (s : String) (p : Char → Bool) (b : String.Pos) (i : String.Pos) (r : List String) :

List String

source

@[specialize]

def String.split (s : String) (p : Char → Bool) :

List String

Equations

String.split s p = String.splitAux s p 0 0 []

source

partial def String.splitOnAux (s : String) (sep : String) (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List String) :

List String

source

def String.splitOn (s : String) (sep : optParam String " ") :

List String

Equations

String.splitOn s sep = if (sep == "") = true then [s] else String.splitOnAux s sep 0 0 0 []

source

instance String.instInhabitedString:

Inhabited String

Equations

String.instInhabitedString = { default := "" }

source

instance String.instAppendString:

Append String

Equations

String.instAppendString = { append := String.append }

source

def String.str:

String → Char → String

Equations

String.str = String.push

source

def String.pushn (s : String) (c : Char) (n : Nat) :

String

Equations

String.pushn s c n = Nat.repeat (fun s => String.push s c) n s

source

def String.isEmpty (s : String) :

Bool

Equations

String.isEmpty s = (String.endPos s == 0)

source

def String.join (l : List String) :

String

Equations

String.join l = List.foldl (fun r s => r ++ s) "" l

source

def String.singleton (c : Char) :

String

Equations

String.singleton c = String.push "" c

source

def String.intercalate (s : String) :

List String → String

Equations

String.intercalate s _fun_discr = match _fun_discr with | [] => "" | a :: as => String.intercalate.go a s as

source

def String.intercalate.go (acc : String) (s : String) :

List String → String

Equations

String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
String.intercalate.go acc s [] = acc

source

structure String.Iterator:

Type

s : String
i : String.Pos

source

instance String.instDecidableEqIterator:

DecidableEq String.Iterator

Equations

String.instDecidableEqIterator = [anonymous]

source

def String.mkIterator (s : String) :

String.Iterator

Equations

String.mkIterator s = { s := s, i := 0 }

source

@[inline]

abbrev String.iter (s : String) :

String.Iterator

Equations

String.iter = String.mkIterator

source

instance String.instSizeOfIterator:

SizeOf String.Iterator

Equations

String.instSizeOfIterator = { sizeOf := fun i => String.utf8ByteSize i.s - i.i.byteIdx }

source

theorem String.Iterator.sizeOf_eq (i : String.Iterator) :

sizeOf i = String.utf8ByteSize i.s - i.i.byteIdx

source

def String.Iterator.toString:

String.Iterator → String

Equations

String.Iterator.toString _fun_discr = match _fun_discr with | { s := s, i := i } => s

source

def String.Iterator.remainingBytes:

String.Iterator → Nat

Equations

String.Iterator.remainingBytes _fun_discr = match _fun_discr with | { s := s, i := i } => (String.endPos s).byteIdx - i.byteIdx

source

def String.Iterator.pos:

String.Iterator → String.Pos

Equations

String.Iterator.pos _fun_discr = match _fun_discr with | { s := s, i := i } => i

source

def String.Iterator.curr:

String.Iterator → Char

Equations

String.Iterator.curr _fun_discr = match _fun_discr with | { s := s, i := i } => String.get s i

source

def String.Iterator.next:

String.Iterator → String.Iterator

Equations

String.Iterator.next _fun_discr = match _fun_discr with | { s := s, i := i } => { s := s, i := String.next s i }

source

def String.Iterator.prev:

String.Iterator → String.Iterator

Equations

String.Iterator.prev _fun_discr = match _fun_discr with | { s := s, i := i } => { s := s, i := String.prev s i }

source

def String.Iterator.atEnd:

String.Iterator → Bool

Equations

String.Iterator.atEnd _fun_discr = match _fun_discr with | { s := s, i := i } => decide (i.byteIdx ≥ (String.endPos s).byteIdx)

source

def String.Iterator.hasNext:

String.Iterator → Bool

Equations

String.Iterator.hasNext _fun_discr = match _fun_discr with | { s := s, i := i } => decide (i.byteIdx < (String.endPos s).byteIdx)

source

def String.Iterator.hasPrev:

String.Iterator → Bool

Equations

String.Iterator.hasPrev _fun_discr = match _fun_discr with | { s := s, i := i } => decide (i.byteIdx > 0)

source

def String.Iterator.setCurr:

String.Iterator → Char → String.Iterator

Equations

String.Iterator.setCurr _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { s := s, i := i }, c => { s := String.set s i c, i := i }

source

def String.Iterator.toEnd:

String.Iterator → String.Iterator

Equations

String.Iterator.toEnd _fun_discr = match _fun_discr with | { s := s, i := i } => { s := s, i := String.endPos s }

source

def String.Iterator.extract:

String.Iterator → String.Iterator → String

Equations

One or more equations did not get rendered due to their size.

source

def String.Iterator.forward:

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.forward _fun_discr 0 = _fun_discr
String.Iterator.forward _fun_discr (Nat.succ n) = String.Iterator.forward (String.Iterator.next _fun_discr) n

source

def String.Iterator.remainingToString:

String.Iterator → String

Equations

String.Iterator.remainingToString _fun_discr = match _fun_discr with | { s := s, i := i } => String.extract s i (String.endPos s)

source

def String.Iterator.nextn:

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.nextn _fun_discr 0 = _fun_discr
String.Iterator.nextn _fun_discr (Nat.succ n) = String.Iterator.nextn (String.Iterator.next _fun_discr) n

source

def String.Iterator.prevn:

String.Iterator → Nat → String.Iterator

Equations

String.Iterator.prevn _fun_discr 0 = _fun_discr
String.Iterator.prevn _fun_discr (Nat.succ n) = String.Iterator.prevn (String.Iterator.prev _fun_discr) n

source

partial def String.offsetOfPosAux (s : String) (pos : String.Pos) (i : String.Pos) (offset : Nat) :

Nat

source

def String.offsetOfPos (s : String) (pos : String.Pos) :

Nat

Equations

String.offsetOfPos s pos = String.offsetOfPosAux s pos 0 0

source

@[specialize]

def String.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :

Equations

String.foldlAux f s stopPos i a = String.foldlAux.loop f s stopPos i a

source

partial def String.foldlAux.loop {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :

source

@[inline]

def String.foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) :

Equations

String.foldl f init s = String.foldlAux f s (String.endPos s) 0 init

source

@[specialize]

def String.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : String.Pos) (i : String.Pos) :

Equations

String.foldrAux f a s stopPos i = String.foldrAux.loop f a s stopPos i

source

partial def String.foldrAux.loop {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : String.Pos) (i : String.Pos) :

source

@[inline]

def String.foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) :

Equations

String.foldr f init s = String.foldrAux f init s (String.endPos s) 0

source

@[specialize]

def String.anyAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) :

Bool

Equations

String.anyAux s stopPos p i = String.anyAux.loop s stopPos p i

source

partial def String.anyAux.loop (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) :

Bool

source

@[inline]

def String.any (s : String) (p : Char → Bool) :

Bool

Equations

String.any s p = String.anyAux s (String.endPos s) p 0

source

@[inline]

def String.all (s : String) (p : Char → Bool) :

Bool

Equations

String.all s p = !String.any s fun c => !p c

source

def String.contains (s : String) (c : Char) :

Bool

Equations

String.contains s c = String.any s fun a => a == c

source

@[specialize]

partial def String.mapAux (f : Char → Char) (i : String.Pos) (s : String) :

String

source

@[inline]

def String.map (f : Char → Char) (s : String) :

String

Equations

String.map f s = String.mapAux f 0 s

source

def String.isNat (s : String) :

Bool

Equations

String.isNat s = (!String.isEmpty s && String.all s fun a => Char.isDigit a)

source

def String.toNat? (s : String) :

Option Nat

Equations

String.toNat? s = if String.isNat s = true then some (String.foldl (fun n c => n * 10 + (Char.toNat c - Char.toNat (Char.ofNat 48))) 0 s) else none

source

def String.substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) :

Bool

Return true iff the substring of byte size sz starting at position off1 in s1 is equal to that starting at off2 in s2.. False if either substring of that byte size does not exist.

Equations

One or more equations did not get rendered due to their size.

source

partial def String.substrEq.loop (s1 : String) (s2 : String) (off1 : String.Pos) (off2 : String.Pos) (stop1 : String.Pos) :

Bool

source

def String.isPrefixOf (p : String) (s : String) :

Bool

Return true iff p is a prefix of s

Equations

String.isPrefixOf p s = String.substrEq p 0 s 0 (String.endPos p).byteIdx

source

def String.replace (s : String) (pattern : String) (replacement : String) :

String

Replace all occurrences of pattern in s with replacment.

Equations

String.replace s pattern replacement = String.replace.loop s pattern replacement "" 0 0

source

partial def String.replace.loop (s : String) (pattern : String) (replacement : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) :

String

source

@[inline]

def Substring.isEmpty (ss : Substring) :

Bool

Equations

Substring.isEmpty ss = (Substring.bsize ss == 0)

source

@[inline]

def Substring.toString:

Substring → String

Equations

Substring.toString _fun_discr = match _fun_discr with | { str := s, startPos := b, stopPos := e } => String.extract s b e

source

@[inline]

def Substring.toIterator:

Substring → String.Iterator

Equations

Substring.toIterator _fun_discr = match _fun_discr with | { str := s, startPos := b, stopPos := stopPos } => { s := s, i := b }

source

@[inline]

def Substring.get:

Substring → String.Pos → Char

Return the codepoint at the given offset into the substring.

Equations

Substring.get _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { str := s, startPos := b, stopPos := stopPos }, p => String.get s (b + p)

source

@[inline]

def Substring.next:

Substring → String.Pos → String.Pos

Given an offset of a codepoint into the substring, return the offset there of the next codepoint.

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Substring.prev:

Substring → String.Pos → String.Pos

Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.

Equations

One or more equations did not get rendered due to their size.

source

def Substring.nextn:

Substring → Nat → String.Pos → String.Pos

Equations

Substring.nextn _fun_discr 0 _fun_discr = _fun_discr
Substring.nextn _fun_discr (Nat.succ i) _fun_discr = Substring.nextn _fun_discr i (Substring.next _fun_discr _fun_discr)

source

def Substring.prevn:

Substring → Nat → String.Pos → String.Pos

Equations

Substring.prevn _fun_discr 0 _fun_discr = _fun_discr
Substring.prevn _fun_discr (Nat.succ i) _fun_discr = Substring.prevn _fun_discr i (Substring.prev _fun_discr _fun_discr)