mathlib documentation

core / init.meta.options

meta constant options  :
Type
Instances for options
meta constant options.size  :
meta constant options.mk  :
meta constant options.contains  :
optionsnamebool
meta constant options.set_bool  :
optionsnamebooloptions
meta constant options.set_nat  :
optionsnameoptions
meta constant options.set_string  :
meta constant options.get_bool  :
optionsnameboolbool
meta constant options.get_nat  :
optionsname
meta constant options.get_string  :
meta constant options.join  :
meta constant options.fold {α : Type u} :
optionsα → (nameα → α) → α
@[instance]
@[protected, instance]
@[protected, instance]