INNER CODE UNIT · Python

lookup

lean-dojo/TorchLean · scripts/generate_unicode_table.py:207

def lookup? (char : Char) : Option Interval :=
  search char.val intervals.size 0 intervals.size
where
  search (codepoint : UInt32) : (fuel lo hi : Nat) → Option Interval
    | 0, _, _ => none
    | fuel + 1, lo, hi =>
        if lo < hi then
          let mid := (lo + hi) / 2
          match intervals[mid]? with
          | none => none
          | some interval =>
              if codepoint < interval.lo then
                search codepoint fuel lo mid
              else if interval.hi < codepoint then
                search codepoint fuel (mid + 1) hi
              else
                some interval
        else

View source record →