Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2019 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Keeley Hoek, Floris van Doorn, Chris Bailey

! This file was ported from Lean 3 source module data.string.defs
! leanprover-community/mathlib commit e7131068d9696deec51e6cd7668b6d9ac69af6a4
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Data.List.Basic
import Mathlib.Mathport.Rename

/-!
# Definitions for `String`

This file defines a bunch of functions for the `String` datatype.
-/

namespace String

#align string.split_on 
String.splitOn: String โ†’ optParam String " " โ†’ List String
String.splitOn
#align string.is_prefix_of 
String.isPrefixOf: String โ†’ String โ†’ Bool
String.isPrefixOf
#align string.starts_with 
String.startsWith: String โ†’ String โ†’ Bool
String.startsWith
#align string.ends_with 
String.endsWith: String โ†’ String โ†’ Bool
String.endsWith
#align string.is_nat 
String.isNat: String โ†’ Bool
String.isNat

/-- Pad `s : String` with repeated occurrences of `c : Char` until it's of length `n`.
  If `s` is initially larger than `n`, just return `s`. -/
def 
leftpad: Nat โ†’ Char โ†’ String โ†’ String
leftpad (
n: Nat
n : 
Nat: Type
Nat) (
c: Char
c : 
Char: Type
Char) (
s: String
s : 
String: Type
String) : 
String: Type
String :=
  โŸจ
List.leftpad: {ฮฑ : Type ?u.13} โ†’ Nat โ†’ ฮฑ โ†’ List ฮฑ โ†’ List ฮฑ
List.leftpad 
n: Nat
n 
c: Char
c 
s: String
s.
data: String โ†’ List Char
dataโŸฉ

/-- Construct the string consisting of `n` copies of the character `c`. -/
def 
replicate: Nat โ†’ Char โ†’ String
replicate (
n: Nat
n : 
Nat: Type
Nat) (
c: Char
c : 
Char: Type
Char) : 
String: Type
String :=
  โŸจ
List.replicate: {ฮฑ : Type ?u.71} โ†’ Nat โ†’ ฮฑ โ†’ List ฮฑ
List.replicate 
n: Nat
n 
c: Char
cโŸฉ

/-- `s.isPrefix t` checks if the string `s` is a prefix of the string `t`. -/
def 
isPrefix: String โ†’ String โ†’ Prop
isPrefix : 
String: Type
String โ†’ 
String: Type
String โ†’ 
Prop: Type
Prop
| โŸจ
d1: List Char
d1โŸฉ, โŸจ
d2: List Char
d2โŸฉ => 
List.isPrefix: {ฮฑ : Type ?u.132} โ†’ List ฮฑ โ†’ List ฮฑ โ†’ Prop
List.isPrefix 
d1: List Char
d1 
d2: List Char
d2

/-- `s.isSuffix t` checks if the string `s` is a suffix of the string `t`. -/
def 
isSuffix: String โ†’ String โ†’ Prop
isSuffix : 
String: Type
String โ†’ 
String: Type
String โ†’ 
Prop: Type
Prop
| โŸจ
d1: List Char
d1โŸฉ, โŸจ
d2: List Char
d2โŸฉ => 
List.isSuffix: {ฮฑ : Type ?u.266} โ†’ List ฮฑ โ†’ List ฮฑ โ†’ Prop
List.isSuffix 
d1: List Char
d1 
d2: List Char
d2

/-- `String.mapTokens c f s` tokenizes `s : string` on `c : char`, maps `f` over each token, and
then reassembles the string by intercalating the separator token `c` over the mapped tokens. -/
def 
mapTokens: Char โ†’ (String โ†’ String) โ†’ String โ†’ String
mapTokens (
c: Char
c : 
Char: Type
Char) (
f: String โ†’ String
f : 
String: Type
String โ†’ 
String: Type
String) : 
String: Type
String โ†’ 
String: Type
String :=
  
intercalate: String โ†’ List String โ†’ String
intercalate (
singleton: Char โ†’ String
singleton 
c: Char
c) โˆ˜ 
List.map: {ฮฑ : Type ?u.390} โ†’ {ฮฒ : Type ?u.389} โ†’ (ฮฑ โ†’ ฮฒ) โ†’ List ฮฑ โ†’ List ฮฒ
List.map 
f: String โ†’ String
f โˆ˜ (ยท.
split: String โ†’ (Char โ†’ Bool) โ†’ List String
split (ยท = 
c: Char
c))
#align string.map_tokens 
String.mapTokens: Char โ†’ (String โ†’ String) โ†’ String โ†’ String
String.mapTokens

/-- `isPrefixOf? pre s` returns `some post` if `s = pre ++ post`.
If `pre` is not a prefix of `s`, it returns `none`. -/
def 
isPrefixOf?: String โ†’ String โ†’ Option String
isPrefixOf? (
pre: String
pre 
s: String
s : 
String: Type
String) : 
Option: Type ?u.647 โ†’ Type ?u.647
Option 
String: Type
String :=
  if 
startsWith: String โ†’ String โ†’ Bool
startsWith 
s: String
s 
pre: String
pre then 
some: {ฮฑ : Type ?u.741} โ†’ ฮฑ โ†’ Option ฮฑ
some <| 
s: String
s.
drop: String โ†’ Nat โ†’ String
drop 
pre: String
pre.
length: String โ†’ Nat
length else 
none: {ฮฑ : Type ?u.747} โ†’ Option ฮฑ
none

/-- Return true iff `p` is a suffix of `s`. -/
def 
isSuffixOf: String โ†’ String โ†’ Bool
isSuffixOf (
p: String
p 
s: String
s : 
String: Type
String) : 
Bool: Type
Bool :=
  
substrEq: String โ†’ Pos โ†’ String โ†’ Pos โ†’ Nat โ†’ Bool
substrEq 
p: String
p 
0: ?m.812
0 
s: String
s (
s: String
s.
endPos: String โ†’ Pos
endPos - 
p: String
p.
endPos: String โ†’ Pos
endPos) 
p: String
p.
endPos: String โ†’ Pos
endPos.
byteIdx: Pos โ†’ Nat
byteIdx
#align string.is_suffix_of 
String.isSuffixOf: String โ†’ String โ†’ Bool
String.isSuffixOf

/-- `isSuffixOf? suff s` returns `some pre` if `s = pre ++ suff`.
If `suff` is not a suffix of `s`, it returns `none`. -/
def 
isSuffixOf?: String โ†’ String โ†’ Option String
isSuffixOf? (
suff: String
suff 
s: String
s : 
String: Type
String) : 
Option: Type ?u.907 โ†’ Type ?u.907
Option 
String: Type
String :=
  if 
s: String
s.
endsWith: String โ†’ String โ†’ Bool
endsWith 
suff: String
suff then 
some: {ฮฑ : Type ?u.1003} โ†’ ฮฑ โ†’ Option ฮฑ
some <| 
s: String
s.
dropRight: String โ†’ Nat โ†’ String
dropRight 
suff: String
suff.
length: String โ†’ Nat
length else 
none: {ฮฑ : Type ?u.1009} โ†’ Option ฮฑ
none

/-- `s.stripPrefix p` will remove `p` from the beginning of `s` if it occurs there,
or otherwise return `s`. -/
def 
stripPrefix: (s p : String) โ†’ ?m.1066 s p
stripPrefix (
s: String
s 
p: String
p : 
String: Type
String) :=
  if 
s: String
s.
startsWith: String โ†’ String โ†’ Bool
startsWith 
p: String
p then 
s: String
s.
drop: String โ†’ Nat โ†’ String
drop 
p: String
p.
length: String โ†’ Nat
length else 
s: String
s

/-- `s.stripSuffix p` will remove `p` from the end of `s` if it occurs there,
or otherwise return `s`. -/
def 
stripSuffix: (s p : String) โ†’ ?m.1217 s p
stripSuffix (
s: String
s 
p: String
p : 
String: Type
String) :=
  if 
s: String
s.
endsWith: String โ†’ String โ†’ Bool
endsWith 
p: String
p then 
s: String
s.
dropRight: String โ†’ Nat โ†’ String
dropRight 
p: String
p.
length: String โ†’ Nat
length else 
s: String
s

/-- Count the occurrences of a character in a string. -/
def 
count: String โ†’ Char โ†’ Nat
count (
s: String
s : 
String: Type
String) (
c: Char
c : 
Char: Type
Char) : 
Nat: Type
Nat :=
  
s: String
s.
foldl: {ฮฑ : Type ?u.1370} โ†’ (ฮฑ โ†’ Char โ†’ ฮฑ) โ†’ ฮฑ โ†’ String โ†’ ฮฑ
foldl (fun 
n: ?m.1377
n 
d: ?m.1380
d => if 
d: ?m.1380
d = 
c: Char
c then 
n: ?m.1377
n + 
1: ?m.1400
1 else 
n: ?m.1377
n) 
0: ?m.1448
0

/-- `getRest s t` returns `some r` if `s = t ++ r`.
If `t` is not a prefix of `s`, it returns `none`. -/
def 
getRest: String โ†’ String โ†’ Option String
getRest (
s: String
s 
t: String
t : 
String: Type
String) : 
Option: Type ?u.1570 โ†’ Type ?u.1570
Option 
String: Type
String :=
  
List.asString: List Char โ†’ String
List.asString <$> 
s: String
s.
toList: String โ†’ List Char
toList.
getRest: {ฮฑ : Type ?u.1593} โ†’ [inst : DecidableEq ฮฑ] โ†’ List ฮฑ โ†’ List ฮฑ โ†’ Option (List ฮฑ)
getRest 
t: String
t.
toList: String โ†’ List Char
toList
#align string.get_rest 
String.getRest: String โ†’ String โ†’ Option String
String.getRest

#align string.popn 
String.drop: String โ†’ Nat โ†’ String
String.drop

/-- Produce the head character from the string `s`, if `s` is not empty, otherwise `'A'`. -/
def 
head: String โ†’ Char
head (
s: String
s : 
String: Type
String) : 
Char: Type
Char :=
  
s: String
s.
iter: String โ†’ Iterator
iter.
curr: Iterator โ†’ Char
curr
#align string.head 
String.head: String โ†’ Char
String.head

end String