mathlib documentation

core.init.meta.set_get_option_tactics

source
meta def tactic.set_bool_option (n : name) (v : bool) :
tactic unit

source
meta def tactic.set_nat_option (n : name) (v : ℕ) :
tactic unit

source
meta def tactic.set_string_option (n : name) (v : string) :
tactic unit

source
meta def tactic.get_bool_option (n : name) (default : bool) :
tactic bool

source
meta def tactic.get_nat_option (n : name) (default : ℕ) :
tactic ℕ

source
meta def tactic.get_string_option (n : name) (default : string) :
tactic string