mathlib documentation

core / init.meta.set_get_option_tactics

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

meta def tactic.set_nat_option (n : name) (v : ) :

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

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

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