mathlib documentation

core / init.meta.options

source
meta constant options  :
Type
source
meta constant options.size  :
options → ℕ
source
meta constant options.mk  :
options
source
meta constant options.contains  :
options → name → bool
source
meta constant options.set_bool  :
options → name → bool → options
source
meta constant options.set_nat  :
options → name → ℕ → options
source
meta constant options.set_string  :
options → name → string → options
source
meta constant options.get_bool  :
options → name → bool → bool
source
meta constant options.get_nat  :
options → name → ℕ → ℕ
source
meta constant options.get_string  :
options → name → string → string
source
meta constant options.join  :
options → options → options
source
meta constant options.fold {α : Type u} :
options → α → (name → α → α) → α
source
@[instance]
meta constant options.has_decidable_eq  :
decidable_eq options
source
@[protected, instance]
meta def options.has_add  :
has_add options
source
@[protected, instance]
meta def options.inhabited  :
inhabited options