mathlib3 documentation

core / init.meta.options

meta constant options  :
Instances for options
meta constant options.size  :
meta constant options.mk  :
meta constant options.fold {α : Type u} :
options α (name α α) α
@[instance]
@[protected, instance]
@[protected, instance]