run — Mathlib

English

The run operation of the SetM monad yields the underlying Set; it is the identity on sets.

Русский

Операция запуска монадSetM возвращает базовое множество; она является тождественной на множестве.

LaTeX

$$$\mathrm{SetM.run}(s) = s.$$$

Lean4

/-- Evaluates the `SetM` monad, yielding a `Set`.
Implementation note: this is the identity function. -/
protected def run {α : Type*} (s : SetM α) : Set α :=
  s

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