has_reflect α lets you produce an expr from an instance of α. That is, it is a function from α to expr such that the expr has type α.
Instances
- nat.reflect
- unsigned.reflect
- name.reflect
- list.reflect
- punit.reflect
- bool.has_reflect
- prod.has_reflect
- sum.has_reflect
- option.has_reflect
- interactive.loc.has_reflect
- pos.has_reflect
- tactic.interactive.rw_rule.has_reflect
- tactic.interactive.rw_rules_t.has_reflect
- tactic.simp_arg_type.has_reflect
- thunk.has_reflect
- doc_category.has_reflect
- tactic_doc_entry.has_reflect
- binder_info.has_reflect
- congr_arg_kind.has_reflect
- tactic.transparency.has_reflect
- tactic.rcases_patt.has_reflect
- norm_cast.label.has_reflect
- simps_cfg.has_reflect
- to_additive.value_type.has_reflect
- int.has_reflect
- tactic.interactive.mono_selection.has_reflect
- tactic.interactive.rep_arity.has_reflect
- rat.has_reflect
- tactic.abel.normalize_mode.has_reflect
- tactic.ring.normalize_mode.has_reflect
- pos_num.has_reflect
- num.has_reflect
- znum.has_reflect
- tree.has_reflect
- omega.ee.has_reflect
- omega.int.preterm.has_reflect
- omega.int.preform.has_reflect
- omega.nat.preterm.has_reflect
- omega.nat.preform.has_reflect
- tactic.tfae.arrow.has_reflect
- nzsnum.has_reflect
- snum.has_reflect
- tactic.ring2.csring_expr.has_reflect
- string.has_reflect
@[instance]