Reflect a C++ name object. The VM replaces it with the C++ implementation.
Instances for name
@[reducible]
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 = α
@[protected, instance]
Equations
Equations
- mk_num_name n v = name.mk_numeral (unsigned.of_nat' v) n
@[protected, 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 ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_numeral ᾰ ᾰ_1) ++ sep ++ repr v
- name.to_string_with_sep sep (name.mk_numeral v (name.mk_string ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_string ᾰ ᾰ_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 ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_numeral ᾰ ᾰ_1) ++ sep ++ s
- name.to_string_with_sep sep (name.mk_string s (name.mk_string ᾰ ᾰ_1)) = name.to_string_with_sep sep (name.mk_string ᾰ ᾰ_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
@[protected]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- name.has_repr = {repr := name.repr}