Definitions: Mathlib.Init

3 definitions of 1 modules, Mathlib.Init to Mathlib.Init. ‹ previous next ›

Mathlib.Init

linter.mathlibStandardSetopaqueMathlib.Init, function or constant
Wording
no wording
English
$\operatorname{mathlibStandardSet}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.
linter.nightlyRegressionSetopaqueMathlib.Init, function or constant
Wording
no wording
English
$\operatorname{nightlyRegressionSet}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.
linter.weeklyLintSetopaqueMathlib.Init, function or constant
Wording
no wording
English
$\operatorname{weeklyLintSet}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.

‹ previous next ›