How to make a String.nextn function

Stream: general

[Tamas Hadhazy]

For subString we already have Substring.nextn how would I write one from scratch for a String? It only has String.next, which only advances the position by 1

[Kenny Lau]

@Tamas Hadhazy

import Mathlib.Logic.Function.Iterate

set_option autoImplicit false

def s := "áéíóúabcdefg"
def i : String.Pos := 0

#eval s.next^[3] i