Hole.check.width: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/rules/correctness/hole.bend as Hole
Lines 26-34 of bolt@1.27.0.0/src/rules/correctness/hole.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/rules/correctness/hole.bend&start_line=26&end_line=34

import Base
import bolt@1.27.0.0/src/syntax/lex.bend as Lex
import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy

# the width of the hole a `?` at line, col starts: through the next token
# past spaces, newlines and comments when it sits on the same line, else 1
def check.width(toks: List<&2, Lex.Tok>, +line: U32, +col: U32) -> U32:
  match toks:
    case Con{Lex.Tok{k, t, +l, +c}, rest}:
      Lazy.stop(U32, Lex.significant(k), Bool.pick(U32, U32.is_eq(l, line), U32.add(U32.sub(c, col), 4), 1),
        _u => check.width(rest, line, col))
    case Nil{}:
      1

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lazy/lazy.bend&name=stop
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/syntax/lex.bend&name=Tok
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/syntax/lex.bend&name=significant