get? — Mathlib

English

The nth element of a weak sequence is obtained by first dropping n elements and then taking the head.

Русский

n-й элемент слабой последовательности получается сначала отбросив n элементов, затем взяв первый элемент.

LaTeX

$$$$\mathrm{get?}(s,n)=\mathrm{head}(\mathrm{drop}(s,n)).$$$$

Lean4

/-- Get the nth element of `s`. -/
def get? (s : WSeq α) (n : ℕ) : Computation (Option α) :=
  head (drop s n)

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