mathlib documentation

core.init.meta.mk_dec_eq_instance

source
meta def tactic.mk_dec_eq_instance_core  :
tactic unit

source
meta def tactic.mk_dec_eq_instance  :
tactic unit

source
@[instance]
meta def tactic.binder_info.has_decidable_eq  :
decidable_eq binder_info

source
meta def tactic.decidable_eq_derive_handler  :
derive_handler