ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>i : String.Pos<VAR>c : Char<GOAL>0 ≠ i + c
<VAR>s : String<GOAL>String.Pos.Valid s s.endPos
<VAR>cs cs' : List Char<GOAL>String.Pos.Valid { data := cs ++ cs' } { byteIdx := String.utf8Len cs }
<VAR>s : String<VAR>p : String.Pos<GOAL>String.Pos.Valid s p → p ≤ s.endPos
<VAR>s : String<GOAL>s.endPos = 0 ↔ s = ""
<VAR>s : String<GOAL>s.isEmpty = true ↔ s = ""
<VAR>s : List Char<VAR>i p n : Nat<GOAL>String.utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } = String.utf8GetAux s { byteIdx := i } { byteIdx := p }
<VAR>s : List Char<VAR>i p : String.Pos<VAR>c : Char<GOAL>String.utf8GetAux s (i + c) (p + c) = String.utf8GetAux s i p
<VAR>cs cs' : List Char<VAR>i p : Nat<VAR>hp : i + String.utf8Len cs = p<GOAL>String.utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.headD default
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.get { byteIdx := String.utf8Len cs } = cs'.headD default
<VAR>c : Char<VAR>cs : List Char<VAR>i : String.Pos<GOAL>{ data := c :: cs }.get (i + c) = { data := cs }.get i
<VAR>cs cs' : List Char<VAR>i p : Nat<VAR>hp : i + String.utf8Len cs = p<GOAL>String.utf8GetAux? (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.head?
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.get? { byteIdx := String.utf8Len cs } = cs'.head?
<VAR>c' : Char<VAR>cs cs' : List Char<VAR>i p : Nat<VAR>hp : i + String.utf8Len cs = p<GOAL>String.utf8SetAux c' (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs ++ List.modifyHead (fun x => c') cs'
<VAR>cs cs' : List Char<VAR>c' : Char<GOAL>{ data := cs ++ cs' }.set { byteIdx := String.utf8Len cs } c' = { data := cs ++ List.modifyHead (fun x => c') cs' }
<VAR>f : Char → Char<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.modify { byteIdx := String.utf8Len cs } f = { data := cs ++ List.modifyHead f cs' }
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.next { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + (cs'.headD default).utf8Size }
<VAR>cs : List Char<VAR>c : Char<VAR>cs' : List Char<GOAL>{ data := cs ++ c :: cs' }.next { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + c.utf8Size }
<VAR>s : String<VAR>p : String.Pos<GOAL>s.atEnd p = true ↔ s.endPos ≤ p
<VAR>s : String<VAR>p : String.Pos<VAR>h : String.Pos.Valid s p<VAR>h₂ : p < s.endPos<GOAL>String.Pos.Valid s (s.next p)
<VAR>cs cs' : List Char<VAR>c : Char<VAR>i p : Nat<VAR>hp : i + (String.utf8Len cs + c.utf8Size) = p<GOAL>String.utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + String.utf8Len cs }
<VAR>cs : List Char<VAR>c : Char<VAR>cs' : List Char<GOAL>{ data := cs ++ c :: cs' }.prev { byteIdx := String.utf8Len cs + c.utf8Size } = { byteIdx := String.utf8Len cs }
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.prev { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs.dropLast }
<VAR>s : String<GOAL>s.front = s.data.headD default
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.atEnd { byteIdx := String.utf8Len cs } = true ↔ cs' = []
<VAR>s : String<VAR>c : Char<GOAL>s.posOfAux c = s.findAux fun x => x == c
<VAR>s : String<VAR>c : Char<GOAL>s.posOf c = s.find fun x => x == c
<VAR>s : String<VAR>c : Char<GOAL>s.revPosOfAux c = s.revFindAux fun x => x == c
<VAR>s : String<VAR>c : Char<GOAL>s.revPosOf c = s.revFind fun x => x == c
<VAR>p : Char → Bool<VAR>l m r : List Char<GOAL>{ data := l ++ m ++ r }.findAux p { byteIdx := String.utf8Len l + String.utf8Len m } { byteIdx := String.utf8Len l } = { byteIdx := String.utf8Len l + String.utf8Len (List.takeWhile (fun x => !p x) m) }
<VAR>p : Char → Bool<VAR>s : String<GOAL>s.find p = { byteIdx := String.utf8Len (List.takeWhile (fun x => !p x) s.data) }
<VAR>p : Char → Bool<VAR>l r : List Char<GOAL>{ data := l.reverse ++ r }.revFindAux p { byteIdx := String.utf8Len l } = Option.map (fun x => { byteIdx := String.utf8Len x }) (List.dropWhile (fun x => !p x) l).tail?
<VAR>p : Char → Bool<VAR>s : String<GOAL>s.revFind p = Option.map (fun x => { byteIdx := String.utf8Len x }) (List.dropWhile (fun x => !p x) s.data.reverse).tail?
<VAR>l₁ l₂ r₁ r₂ : List Char<VAR>stop p : Nat<VAR>hl₁ : p = String.utf8Len l₁<VAR>hl₂ : p = String.utf8Len l₂<VAR>hstop : stop = min (String.utf8Len l₁ + String.utf8Len r₁) (String.utf8Len l₂ + String.utf8Len r₂)<GOAL>String.firstDiffPos.loop { data := l₁ ++ r₁ } { data := l₂ ++ r₂ } { byteIdx := stop } { byteIdx := p } = { byteIdx := p + String.utf8Len (List.takeWhile₂ (fun x x_1 => decide (x = x_1)) r₁ r₂).fst }
<VAR>a b : String<GOAL>a.firstDiffPos b = { byteIdx := String.utf8Len (List.takeWhile₂ (fun x x_1 => decide (x = x_1)) a.data b.data).fst }
<VAR>s : List Char<VAR>i e n : Nat<GOAL>String.extract.go₂ s { byteIdx := i + n } { byteIdx := e + n } = String.extract.go₂ s { byteIdx := i } { byteIdx := e }
<VAR>s t : List Char<VAR>i e : Nat<GOAL>e = String.utf8Len s + i → String.extract.go₂ (s ++ t) { byteIdx := i } { byteIdx := e } = s
<VAR>s : List Char<VAR>i b e n : Nat<GOAL>String.extract.go₁ s { byteIdx := i + n } { byteIdx := b + n } { byteIdx := e + n } = String.extract.go₁ s { byteIdx := i } { byteIdx := b } { byteIdx := e }
<VAR>c : Char<VAR>cs : List Char<VAR>b e : String.Pos<GOAL>String.extract.go₁ (c :: cs) 0 (b + c) (e + c) = String.extract.go₁ cs 0 b e
<VAR>s t : List Char<VAR>i b : Nat<VAR>e : String.Pos<GOAL>b = String.utf8Len s + i → String.extract.go₁ (s ++ t) { byteIdx := i } { byteIdx := b } e = String.extract.go₂ t { byteIdx := b } e
<VAR>s : List Char<GOAL>String.extract.go₁ s 0 0 { byteIdx := String.utf8Len s } = s
<VAR>c : Char<VAR>cs : List Char<VAR>b e : String.Pos<GOAL>{ data := c :: cs }.extract (b + c) (e + c) = { data := cs }.extract b e
<VAR>s : String<GOAL>s.extract 0 s.endPos = s
<VAR>l m r : List Char<GOAL>{ data := l ++ m ++ r }.extract { byteIdx := String.utf8Len l } { byteIdx := String.utf8Len l + String.utf8Len m } = { data := m }
<VAR>p : Char → Bool<VAR>l m r : List Char<VAR>acc : List String<GOAL>{ data := l ++ m ++ r }.splitAux p { byteIdx := String.utf8Len l } { byteIdx := String.utf8Len l + String.utf8Len m } acc = acc.reverse ++ List.map String.mk (List.splitOnP.go p r m.reverse)
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.split p = List.map String.mk (List.splitOnP p s.data)
<VAR>ss : List String<VAR>cs : List Char<GOAL>List.foldl (fun x x_1 => x ++ x_1) { data := cs } ss = { data := cs ++ (List.map String.data ss).join }
<VAR>ss : List String<GOAL>String.join ss = { data := (List.map String.data ss).join }
<VAR>ss : List String<GOAL>(String.join ss).data = (List.map String.data ss).join
<VAR>c : Char<VAR>cs : List Char<VAR>i : String.Pos<GOAL>{ s := { data := c :: cs }, i := i + c }.hasNext = { s := { data := cs }, i := i }.hasNext
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it.Valid
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it = { s := { data := l.reverseAux r }, i := { byteIdx := String.utf8Len l } }
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it = { s := { data := l.reverse ++ r }, i := { byteIdx := String.utf8Len l.reverse } }
<VAR>l r : List Char<GOAL>String.Iterator.ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := String.utf8Len l.reverse } }
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>it.s.data = l.reverseAux r → it.i.byteIdx = String.utf8Len l → String.Iterator.ValidFor l r it
<VAR>s : String<GOAL>String.Iterator.ValidFor [] s.data s.mkIterator
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it.remainingBytes = String.utf8Len r
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it.s = { data := l.reverseAux r }
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it.i = { byteIdx := String.utf8Len l }
<VAR>l r : List Char<VAR>it : String.Iterator<VAR>h : String.Iterator.ValidFor l r it<GOAL>it.i = 0 ↔ l = []
<VAR>l r : List Char<VAR>it : String.Iterator<VAR>h : String.Iterator.ValidFor l r it<GOAL>it.i = it.s.endPos ↔ r = []
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → it.curr = r.headD default
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l (c :: r) it → String.Iterator.ValidFor (c :: l) r it.next
<VAR>c : Char<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor (c :: l) r it → String.Iterator.ValidFor l (c :: r) it.prev
<VAR>r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor [] r it → String.Iterator.ValidFor [] r it.prev
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → (it.atEnd = true ↔ r = [])
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → (it.hasNext = true ↔ r ≠ [])
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → (it.hasPrev = true ↔ l ≠ [])
<VAR>l r : List Char<VAR>c : Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → String.Iterator.ValidFor l (List.modifyHead (fun x => c) r) (it.setCurr c)
<VAR>l : List Char<VAR>c : Char<VAR>r : List Char<VAR>it : String.Iterator<VAR>h : String.Iterator.ValidFor l (c :: r) it<GOAL>String.Iterator.ValidFor l (c :: r) (it.setCurr c)
<VAR>l r : List Char<VAR>it : String.Iterator<VAR>h : String.Iterator.ValidFor l r it<GOAL>String.Iterator.ValidFor (r.reverse ++ l) [] it.toEnd
<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor it.s.data.reverse [] it.toEnd
<VAR>l m r : List Char<VAR>it₁ it₂ : String.Iterator<VAR>h₁ : String.Iterator.ValidFor l (m ++ r) it₁<VAR>h₂ : String.Iterator.ValidFor (m.reverse ++ l) r it₂<GOAL>it₁.extract it₂ = { data := m }
<VAR>l r : List Char<VAR>it : String.Iterator<VAR>h : String.Iterator.ValidFor l r it<GOAL>it.remainingToString = { data := r }
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → ∀ (n : Nat), n ≤ r.length → String.Iterator.ValidFor ((List.take n r).reverse ++ l) (List.drop n r) (it.nextn n)
<VAR>l r : List Char<VAR>it : String.Iterator<GOAL>String.Iterator.ValidFor l r it → ∀ (n : Nat), n ≤ l.length → String.Iterator.ValidFor (List.drop n l) ((List.take n l).reverse ++ r) (it.prevn n)
<VAR>it : String.Iterator<GOAL>it.Valid → ∃ l r, String.Iterator.ValidFor l r it
<VAR>it : String.Iterator<GOAL>it.Valid → it.remainingBytes ≤ it.s.utf8ByteSize
<VAR>it : String.Iterator<GOAL>it.Valid → it.hasNext = true → it.next.Valid
<VAR>it : String.Iterator<GOAL>it.Valid → it.prev.Valid
<VAR>c : Char<VAR>it : String.Iterator<GOAL>it.Valid → (it.setCurr c).Valid
<VAR>it : String.Iterator<VAR>h : it.Valid<VAR>n : Nat<GOAL>(it.prevn n).Valid
<VAR>l m r : List Char<VAR>n : Nat<GOAL>{ data := l ++ m ++ r }.offsetOfPosAux { byteIdx := String.utf8Len l + String.utf8Len m } { byteIdx := String.utf8Len l } n = n + m.length
<VAR>l r : List Char<GOAL>{ data := l ++ r }.offsetOfPos { byteIdx := String.utf8Len l } = l.length
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>l m r : List Char<VAR>a : α<GOAL>String.foldlAux f { data := l ++ m ++ r } { byteIdx := String.utf8Len l + String.utf8Len m } { byteIdx := String.utf8Len l } a = List.foldl f a m
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>s : String<VAR>a : α<GOAL>String.foldl f a s = List.foldl f a s.data
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>l m r : List Char<VAR>a : α<GOAL>String.foldrAux f a { data := l ++ m ++ r } { byteIdx := String.utf8Len l + String.utf8Len m } { byteIdx := String.utf8Len l } = List.foldr f a m
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>s : String<VAR>a : α<GOAL>String.foldr f a s = List.foldr f a s.data
<VAR>p : Char → Bool<VAR>l m r : List Char<GOAL>{ data := l ++ m ++ r }.anyAux { byteIdx := String.utf8Len l + String.utf8Len m } p { byteIdx := String.utf8Len l } = m.any p
<VAR>f : Char → Char<VAR>l r : List Char<GOAL>String.mapAux f { byteIdx := String.utf8Len l } { data := l ++ r } = { data := l ++ List.map f r }
<VAR>f : Char → Char<VAR>s : String<GOAL>String.map f s = { data := List.map f s.data }
<VAR>p : Char → Bool<VAR>l m r : List Char<GOAL>Substring.takeWhileAux { data := l ++ m ++ r } { byteIdx := String.utf8Len l + String.utf8Len m } p { byteIdx := String.utf8Len l } = { byteIdx := String.utf8Len l + String.utf8Len (List.takeWhile p m) }
<VAR>s : Substring<VAR>self : s.Valid<GOAL>String.Pos.Valid s.str s.stopPos
<VAR>s : Substring<VAR>self : s.Valid<GOAL>s.startPos ≤ s.stopPos
<VAR>s : Substring<VAR>self : s.Valid<GOAL>String.Pos.Valid s.str s.startPos
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.Valid
<VAR>l m r : List Char<VAR>s : Substring<GOAL>s.str.data = l ++ m ++ r → s.startPos.byteIdx = String.utf8Len l → s.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → Substring.ValidFor l m r s
<VAR>s : String<GOAL>Substring.ValidFor [] s.data [] s.toSubstring
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.str = { data := l ++ m ++ r }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.startPos = { byteIdx := String.utf8Len l }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.stopPos = { byteIdx := String.utf8Len l + String.utf8Len m }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.bsize = String.utf8Len m
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → (s.isEmpty = true ↔ m = [])
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.toString = { data := m }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → String.Iterator.ValidFor l.reverse (m ++ r) s.toIterator
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (m₁ ++ c :: m₂) r s → s.get { byteIdx := String.utf8Len m₁ } = c
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (m₁ ++ c :: m₂) r s → s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.next { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (m₁ ++ c :: m₂) r s → s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }
<VAR>l m₁ m₂ r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (m₁ ++ m₂) r s → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }
<VAR>l m₂ r m₁ : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (m₁.reverse ++ m₂) r s → ∀ (n : Nat), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }
<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l (c :: m) r s → s.front = c
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → ∀ (n : Nat), Substring.ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)
<VAR>l m r : List Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → ∀ (n : Nat), Substring.ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)
<VAR>l m r : List Char<VAR>p : Nat<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → (s.atEnd { byteIdx := p } = true ↔ p = String.utf8Len m)
<VAR>l m r ml mm mr : List Char<VAR>b e : String.Pos<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → Substring.ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e } → ∃ l' r', Substring.ValidFor l' mm r' (s.extract b e)
<VAR>α : Type u_1<VAR>l m r : List Char<VAR>f : α → Char → α<VAR>init : α<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → Substring.foldl f init s = List.foldl f init m
<VAR>α : Type u_1<VAR>l m r : List Char<VAR>f : Char → α → α<VAR>init : α<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → Substring.foldr f init s = List.foldr f init m
<VAR>l m r : List Char<VAR>f : Char → Bool<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.any f = m.any f
<VAR>l m r : List Char<VAR>f : Char → Bool<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → s.all f = m.all f
<VAR>l m r : List Char<VAR>c : Char<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → (s.contains c = true ↔ c ∈ m)
<VAR>l m r : List Char<VAR>p : Char → Bool<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → Substring.ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) (s.takeWhile p)
<VAR>l m r : List Char<VAR>p : Char → Bool<VAR>s : Substring<GOAL>Substring.ValidFor l m r s → Substring.ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r (s.dropWhile p)
<VAR>s : Substring<GOAL>s.Valid → ∃ l m r, Substring.ValidFor l m r s
<VAR>s : Substring<GOAL>s.Valid → s.bsize = String.utf8Len s.toString.data
<VAR>s : Substring<GOAL>s.Valid → (s.isEmpty = true ↔ s.toString = "")
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.get { byteIdx := String.utf8Len m₁ } = c
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }
<VAR>s : Substring<GOAL>s.Valid → s.next { byteIdx := s.bsize } = { byteIdx := s.bsize }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }
<VAR>s : Substring<GOAL>s.Valid → ∀ (n : Nat), s.nextn n { byteIdx := s.bsize } = { byteIdx := s.bsize }
<VAR>m₁ m₂ : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = m₁ ++ m₂ → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }
<VAR>m₂ m₁ : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = m₁.reverse ++ m₂ → ∀ (n : Nat), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }
<VAR>c : Char<VAR>m : List Char<VAR>s : Substring<GOAL>s.Valid → s.toString.data = c :: m → s.front = c
<VAR>s : Substring<GOAL>s.Valid → ∀ (n : Nat), (s.drop n).Valid
<VAR>s : Substring<GOAL>s.Valid → ∀ (n : Nat), (s.drop n).toString.data = List.drop n s.toString.data
<VAR>s : Substring<GOAL>s.Valid → ∀ (n : Nat), (s.take n).Valid
<VAR>s : Substring<GOAL>s.Valid → ∀ (n : Nat), (s.take n).toString.data = List.take n s.toString.data
<VAR>p : Nat<VAR>s : Substring<GOAL>s.Valid → (s.atEnd { byteIdx := p } = true ↔ p = s.toString.utf8ByteSize)
<VAR>b e : String.Pos<VAR>s : Substring<GOAL>s.Valid → { str := s.toString, startPos := b, stopPos := e }.Valid → (s.extract b e).Valid
<VAR>b e : String.Pos<VAR>s : Substring<GOAL>s.Valid → { str := s.toString, startPos := b, stopPos := e }.Valid → (s.extract b e).toString = s.toString.extract b e
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>init : α<VAR>s : Substring<GOAL>s.Valid → Substring.foldl f init s = List.foldl f init s.toString.data
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>init : α<VAR>s : Substring<GOAL>s.Valid → Substring.foldr f init s = List.foldr f init s.toString.data
<VAR>f : Char → Bool<VAR>s : Substring<GOAL>s.Valid → s.any f = s.toString.data.any f
<VAR>f : Char → Bool<VAR>s : Substring<GOAL>s.Valid → s.all f = s.toString.data.all f
<VAR>c : Char<VAR>s : Substring<GOAL>s.Valid → (s.contains c = true ↔ c ∈ s.toString.data)
<VAR>p : Char → Bool<VAR>s : Substring<GOAL>s.Valid → (s.takeWhile p).Valid
<VAR>p : Char → Bool<VAR>s : Substring<GOAL>s.Valid → (s.takeWhile p).toString.data = List.takeWhile p s.toString.data
<VAR>p : Char → Bool<VAR>s : Substring<GOAL>s.Valid → (s.dropWhile p).Valid
<VAR>p : Char → Bool<VAR>s : Substring<GOAL>s.Valid → (s.dropWhile p).toString.data = List.dropWhile p s.toString.data
<VAR>s : String<VAR>n : Nat<GOAL>s.drop n = { data := List.drop n s.data }
<VAR>s : String<VAR>n : Nat<GOAL>s.take n = { data := List.take n s.data }
<VAR>p : Char → Bool<VAR>s : String<GOAL>s.takeWhile p = { data := List.takeWhile p s.data }
<VAR>p : Char → Bool<VAR>s : String<GOAL>s.dropWhile p = { data := List.dropWhile p s.data }
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>f : β → α → m β<VAR>b : β<GOAL>List.foldlM f b List.nil = pure b
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>f : β → α → m β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>List.foldlM f b (a :: l) = do let init ← f b a List.foldlM f init l
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m β<VAR>b : β<GOAL>List.foldrM f b List.nil = pure b
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>b : β<GOAL>forIn List.nil b f = pure b
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>a : α<VAR>as : List α<VAR>b : β<GOAL>forIn (a :: as) b f = do let x ← f a b match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type v → Type w<VAR>Monad m<VAR>as : List α<VAR>init : β<VAR>f : α → β → m (ForInStep β)<GOAL>(forIn' as init fun a x b => f a b) = forIn as init f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>Monad m<VAR>f : α → m PUnit<GOAL>forM List.nil f = pure PUnit.unit
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>Monad m<VAR>f : α → m PUnit<VAR>a : α<VAR>as : List α<GOAL>forM (a :: as) f = do f a forM as f
<VAR>α : Type u_1<VAR>Inhabited α<VAR>n : Nat<GOAL>[].get! n = default
<VAR>α : Type u_1<VAR>Inhabited α<VAR>l : List α<VAR>a : α<VAR>n : Nat<GOAL>(a :: l).get! (n + 1) = l.get! n
<VAR>α : Type u_1<VAR>Inhabited α<VAR>l : List α<VAR>a : α<GOAL>(a :: l).get! 0 = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l).tail! = l
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : List α<VAR>h : i < as.length<VAR>h' : i < (as ++ bs).length<GOAL>(as ++ bs)[i] = as[i]
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : List α<VAR>h : ¬i < as.length<VAR>h' : i < (as ++ bs).length<VAR>h'' : i - as.length < bs.length<GOAL>(as ++ bs)[i] = bs[i - as.length]
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<VAR>i : Fin (as ++ [a]).length<VAR>h : ¬↑i < as.length<GOAL>(as ++ [a]).get i = a
<VAR>α : Type u_1<VAR>a : α<VAR>SizeOf α<VAR>as : List α<VAR>h : a ∈ as<GOAL>sizeOf a < sizeOf as
<VAR>α : Type u_1<VAR>as bs cs : List α<VAR>h : as ++ bs = as ++ cs<GOAL>bs = cs
<VAR>α : Type u_1<VAR>as bs cs : List α<VAR>h : as ++ bs = cs ++ bs<GOAL>as = cs
<VAR>α : Type u_1<VAR>as bs cs : List α<GOAL>(as ++ bs = as ++ cs) = (bs = cs)
<VAR>α : Type u_1<VAR>as bs cs : List α<GOAL>(as ++ bs = cs ++ bs) = (as = cs)
<VAR>α : Type u_1<VAR>SizeOf α<VAR>as : List α<VAR>i : Fin as.length<GOAL>sizeOf (as.get i) < sizeOf as
<VAR>α : Type u_1<VAR>LT α<VAR>s : Antisymm fun x x_1 => ¬x < x_1<VAR>as bs : List α<VAR>h₁ : as ≤ bs<VAR>h₂ : bs ≤ as<GOAL>as = bs
<VAR>m n : Lean.Name<GOAL>(m == n) = true ↔ m = n
<VAR>m n : Nat<VAR>h : n - m = 0<GOAL>Int.subNatNat m n = ↑(m - n)
<VAR>m n k : Nat<VAR>h : n - m = k.succ<GOAL>Int.subNatNat m n = Int.negSucc k
<VAR>n m : Nat<GOAL>↑(n + m) = ↑n + ↑m
<VAR>n m : Nat<GOAL>↑(n * m) = ↑n * ↑m
<VAR>n : Nat<GOAL>↑n.succ = ↑n + 1
<VAR>n : Nat<GOAL>-↑n.succ = Int.negSucc n
<VAR>n : Nat<GOAL>-Int.negSucc n = ↑n.succ
<VAR>n : Nat<GOAL>Int.negSucc n = -↑(n + 1)
<VAR>n : Nat<GOAL>Int.negOfNat n = -Int.ofNat n
<VAR>m n : Nat<GOAL>↑m + ↑n = ↑(m + n)
<VAR>m n : Nat<GOAL>↑m + Int.negSucc n = Int.subNatNat m n.succ
<VAR>m n : Nat<GOAL>Int.negSucc m + ↑n = Int.subNatNat n m.succ
<VAR>m n : Nat<GOAL>Int.negSucc m + Int.negSucc n = Int.negSucc (m + n).succ
<VAR>m n : Nat<GOAL>↑m * ↑n = ↑(m * n)
<VAR>m n : Nat<GOAL>↑m * Int.negSucc n = Int.negOfNat (m * n.succ)
<VAR>m n : Nat<GOAL>Int.negSucc m * ↑n = Int.negOfNat (m.succ * n)
<VAR>m n : Nat<GOAL>Int.negSucc m * Int.negSucc n = Int.ofNat (m.succ * n.succ)
<VAR>m n : Nat<GOAL>↑m = ↑n ↔ m = n
<VAR>n : Nat<GOAL>↑n = 0 ↔ n = 0
<VAR>n : Nat<GOAL>↑n ≠ 0 ↔ n ≠ 0
<VAR>m n : Nat<GOAL>Int.negSucc m = Int.negSucc n ↔ m = n
<VAR>n : Nat<GOAL>Int.negSucc n = -(↑n + 1)
<VAR>n : Nat<GOAL>Int.negSucc n ≠ 0
<VAR>n : Nat<GOAL>0 ≠ Int.negSucc n
<VAR>n : Nat<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n