thinkN — Mathlib

English

thinkN c n delays the computation c by n steps and then performs c.

Русский

thinkN c n задерживает выполнение вычисления c на n шагов, затем выполняет c.

LaTeX

$$$\\text{thinkN}(c,n) = \\begin{cases} c,& n=0 \\\\ \\text{think}(\\text{thinkN}(c,n-1)),& n>0 \\end{cases}$$$

Lean4

/-- `thinkN c n` is the computation that delays for `n` ticks and then performs
  computation `c`. -/
def thinkN (c : Computation α) : ℕ → Computation α
  | 0 => c
  | n + 1 =>
    think
      (thinkN c n)
        -- check for immediate result

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