ofRat — Mathlib

English

The function ofRat converts a rational to a FP.Float by selecting among nearby finite representations (low, high) and applying a tie-breaking rule; if neither finite is suitable, it returns infinity depending on the mode.

Русский

Функция ofRat преобразует рациональное число в Float, выбирая между соседними конечными представлениями и применяя правило разрешения пересечений; если ни одно конечное не подходит, возвращается бесконечность в зависимости от режима.

LaTeX

$$$\\mathrm{ofRat}:\\mathrm{RMode} \\to \\mathbb{Q} \\to \\mathrm{FP.Float}$ with near-to-rational selection rules$$

Lean4

@[nolint docBlame]
unsafe def ofRat : RMode → ℚ → Float
  | RMode.NE, r =>
    let low := ofRatDn r
    let high := ofRatUp r
    if hf : high.isFinite then
      if r = toRat _ hf then high
      else
        if lf : low.isFinite then
          if r - toRat _ lf > toRat _ hf - r then high
          else
            if r - toRat _ lf < toRat _ hf - r then low
            else
              match low, lf with
              | Float.finite _ _ m _, _ => if 2 ∣ m then low else high
        else Float.inf true
    else Float.inf false

Похожие утверждения