Gadget for automatic parameter support. This is similar to the opt_param gadget, but it uses the tactic declaration names tac_name to synthesize the argument. Like opt_param, this gadget only affects elaboration. For example, the tactic will not be invoked during type class resolution.
Equations
- auto_param α tac_name = α
Instances
@[instance]
Equations
Equations
- mk_num_name n v = name.mk_numeral (unsigned.of_nat' v) n
@[instance]
Equations
Equations
- (name.mk_numeral s p).get_prefix = p
- (name.mk_string s p).get_prefix = p
- name.anonymous.get_prefix = name.anonymous
Equations
- (name.mk_numeral s p).update_prefix new_p = name.mk_numeral s new_p
- (name.mk_string s p).update_prefix new_p = name.mk_string s new_p
- name.anonymous.update_prefix new_p = name.anonymous
Equations
- name.to_string_with_sep sep (name.mk_numeral v (name.mk_numeral a a_1)) = name.to_string_with_sep sep (name.mk_numeral a a_1) ++ sep ++ repr v
- name.to_string_with_sep sep (name.mk_numeral v (name.mk_string a a_1)) = name.to_string_with_sep sep (name.mk_string a a_1) ++ sep ++ repr v
- name.to_string_with_sep sep (name.mk_numeral v name.anonymous) = repr v
- name.to_string_with_sep sep (name.mk_string s (name.mk_numeral a a_1)) = name.to_string_with_sep sep (name.mk_numeral a a_1) ++ sep ++ s
- name.to_string_with_sep sep (name.mk_string s (name.mk_string a a_1)) = name.to_string_with_sep sep (name.mk_string a a_1) ++ sep ++ s
- name.to_string_with_sep sep (name.mk_string s name.anonymous) = s
- name.to_string_with_sep sep name.anonymous = "[anonymous]"
Equations
- n.components = (name.components' n).reverse
@[instance]
Equations
name.append_after n i return a name of the form n_i