Manipulating ranges in the new string API

Stream: lean4

[Michael Rothgang]

The new string API is surely great... but it broke an in-progress linter in mathlib. Can somebody help me fix this (or tell me everything that's wrong with the code below)? A pointer to the right place in the docs would already help.

Here's the minimised code: we check if a string has the shape we want, and if not log an error at a particular place. The previous code used a fair number of by-hand manipulation of ranges, which breaks. Help with the proper way is appreciated!

import Lean
-- placeholder; the actual function is Mathlib.Linter.copyrightHeaderChecks
def stub (copyright : String) : Array (Lean.Syntax × String) := sorry

open Lean Elab Command in
elab "#check_copyright " copStx:str : command => do
  let cop := copStx.getString
  let offset := copStx.raw.getPos?.get! + ⟨1⟩ -- this addition breaks
  for (s, m) in stub cop do
    if let some rg := s.getRange? then
      Lean.logInfoAt (.ofRange ({start := rg.start + offset, stop := rg.stop + offset})) -- this line also breaks
        m!"Text: `<placeholder>`\n\
           Range: {(rg.start, rg.stop)}\n\
           Message: `<placeholder>`"

#check_copyright "Foo" -- fails now, with an error `elaboration function for `«command#check_copyright_»` has not been implemented`

[Michael Rothgang]

(I'm not the original author, but would like to help getting it merged.)

[Markus Himmel]

Use .increaseBy 1 instead of + ⟨1⟩ and .offsetBy offset instead of + offset.

[Michael Rothgang]

Thanks a lot!