jcommelin · July 7, 2020 16:59
diff --git a/typeclass.stats b/typeclass.stats
 { "nodes" : 

 [{ "name" : "partial_order",
 "topic" : "core",
 "file" : "core/init/algebra/order.lean",
 "line" : 26 }
 , { "name" : "has_coe_t_aux",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 123 }
 , { "name" : "is_cond_left_inv",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 55 }
 , { "name" : "is_total",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 95 }
 , { "name" : "has_ssubset",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 340 }
 , { "name" : "has_andthen",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 334 }
 , { "name" : "is_cond_right_inv",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 58 }
 , { "name" : "is_symm_op",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 10 }
 , { "name" : "monad_reader",
 "topic" : "core",
 "file" : "core/init/control/reader.lean",
 "line" : 83 }
 , { "name" : "monad_reader_adapter",
 "topic" : "core",
 "file" : "core/init/control/reader.lean",
 "line" : 106 }
 , { "name" : "add_comm_group",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 301 }
 , { "name" : "add_left_cancel_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 106 }
 , { "name" : "is_preorder",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 98 }
 , { "name" : "has_pow",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 353 }
 , { "name" : "has_coe",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 38 }
 , { "name" : "comm_group",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 298 }
 , { "name" : "is_right_id",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 25 }
 , { "name" : "has_div",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 328 }
 , { "name" : "has_mul",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 324 }
 , { "name" : "interactive.executor",
 "topic" : "core",
 "file" : "core/init/meta/tactic.lean",
 "line" : 102 }
 , { "name" : "is_lawful_functor",
 "topic" : "core",
 "file" : "core/init/control/lawful.lean",
 "line" : 16 }
 , { "name" : "is_distinct",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 61 }
 , { "name" : "has_seq_left",
 "topic" : "core",
 "file" : "core/init/control/applicative.lean",
 "line" : 21 }
 , { "name" : "is_refl",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 77 }
 , { "name" : "is_left_cancel",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 34 }
 , { "name" : "has_dvd",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 329 }
 , { "name" : "left_cancel_monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 212 }
 , { "name" : "has_sep",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 348 }
 , { "name" : "is_associative",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 19 }
 , { "name" : "is_trans",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 92 }
 , { "name" : "has_union",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 335 }
 , { "name" : "is_comm_applicative",
 "topic" : "control",
 "file" : "control/basic.lean",
 "line" : 195 }
 , { "name" : "add_left_cancel_monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 218 }
 , { "name" : "has_sdiff",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 337 }
 , { "name" : "has_subset",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 339 }
 , { "name" : "lean.parser.reflectable",
 "topic" : "core",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 30 }
 , { "name" : "has_bind",
 "topic" : "core",
 "file" : "core/init/control/monad.lean",
 "line" : 12 }
 , { "name" : "has_to_pexpr",
 "topic" : "core",
 "file" : "core/init/meta/pexpr.lean",
 "line" : 33 }
 , { "name" : "is_left_null",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 28 }
 , { "name" : "is_irrefl",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 74 }
 , { "name" : "is_idempotent",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 40 }
 , { "name" : "monad_state",
 "topic" : "core",
 "file" : "core/init/control/state.lean",
 "line" : 94 }
 , { "name" : "has_append",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 333 }
 , { "name" : "subsingleton",
 "topic" : "core",
 "file" : "core/init/logic.lean",
 "line" : 802 }
 , { "name" : "monad_state_adapter",
 "topic" : "core",
 "file" : "core/init/control/state.lean",
 "line" : 159 }
 , { "name" : "has_singleton",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 346 }
 , { "name" : "has_add",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 323 }
 , { "name" : "is_left_id",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 22 }
 , { "name" : "is_strict_weak_order",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 119 }
 , { "name" : "decidable_linear_order",
 "topic" : "core",
 "file" : "core/init/algebra/order.lean",
 "line" : 215 }
 , { "name" : "is_lawful_singleton",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 404 }
 , { "name" : "is_right_cancel",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 37 }
 , { "name" : "is_commutative",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 13 }
 , { "name" : "has_neg",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 326 }
 , { "name" : "has_insert",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 345 }
 , { "name" : "is_linear_order",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 108 }
 , { "name" : "is_left_inv",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 49 }
 , { "name" : "add_right_cancel_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 139 }
 , { "name" : "is_right_inv",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 52 }
 , { "name" : "add_group",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 230 }
 , { "name" : "has_monad_lift",
 "topic" : "core",
 "file" : "core/init/control/lift.lean",
 "line" : 21 }
 , { "name" : "has_to_string",
 "topic" : "core",
 "file" : "core/init/data/to_string.lean",
 "line" : 19 }
 , { "name" : "is_symm",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 80 }
 , { "name" : "linear_order",
 "topic" : "core",
 "file" : "core/init/algebra/order.lean",
 "line" : 30 }
 , { "name" : "has_coe_to_sort",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 48 }
 , { "name" : "nonempty",
 "topic" : "core",
 "file" : "core/init/logic.lean",
 "line" : 788 }
 , { "name" : "has_inter",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 336 }
 , { "name" : "alternative",
 "topic" : "core",
 "file" : "core/init/control/alternative.lean",
 "line" : 15 }
 , { "name" : "comm_monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 203 }
 , { "name" : "has_repr",
 "topic" : "core",
 "file" : "core/init/data/repr.lean",
 "line" : 29 }
 , { "name" : "has_le",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 331 }
 , { "name" : "group",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 226 }
 , { "name" : "reflected",
 "topic" : "core",
 "file" : "core/init/meta/expr.lean",
 "line" : 260 }
 , { "name" : "applicative",
 "topic" : "core",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "is_antisymm",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 89 }
 , { "name" : "monad_functor",
 "topic" : "core",
 "file" : "core/init/control/lift.lean",
 "line" : 50 }
 , { "name" : "has_sizeof",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 464 }
 , { "name" : "monad_except",
 "topic" : "core",
 "file" : "core/init/control/except.lean",
 "line" : 99 }
 , { "name" : "comm_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 76 }
 , { "name" : "has_coe_to_fun",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 45 }
 , { "name" : "has_mod",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 330 }
 , { "name" : "has_zero",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 321 }
 , { "name" : "monad_functor_t",
 "topic" : "core",
 "file" : "core/init/control/lift.lean",
 "line" : 56 }
 , { "name" : "functor",
 "topic" : "core",
 "file" : "core/init/control/functor.lean",
 "line" : 11 }
 , { "name" : "is_per",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 112 }
 , { "name" : "add_comm_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 81 }
 , { "name" : "has_seq_right",
 "topic" : "core",
 "file" : "core/init/control/applicative.lean",
 "line" : 26 }
 , { "name" : "add_comm_monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 207 }
 , { "name" : "preorder",
 "topic" : "core",
 "file" : "core/init/algebra/order.lean",
 "line" : 19 }
 , { "name" : "is_strict_order",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 114 }
 , { "name" : "monad",
 "topic" : "core",
 "file" : "core/init/control/monad.lean",
 "line" : 23 }
 , { "name" : "has_coe_t",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 42 }
 , { "name" : "monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 166 }
 , { "name" : "has_emptyc",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 344 }
 , { "name" : "has_lift",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 31 }
 , { "name" : "has_one",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 322 }
 , { "name" : "has_to_format",
 "topic" : "core",
 "file" : "core/init/meta/format.lean",
 "line" : 70 }
 , { "name" : "has_seq",
 "topic" : "core",
 "file" : "core/init/control/applicative.lean",
 "line" : 16 }
 , { "name" : "decidable",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 275 }
 , { "name" : "is_strict_total_order",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 124 }
 , { "name" : "has_pure",
 "topic" : "core",
 "file" : "core/init/control/applicative.lean",
 "line" : 11 }
 , { "name" : "monad_except_adapter",
 "topic" : "core",
 "file" : "core/init/control/except.lean",
 "line" : 129 }
 , { "name" : "is_total_preorder",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 100 }
 , { "name" : "is_asymm",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 86 }
 , { "name" : "right_cancel_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 133 }
 , { "name" : "is_partial_order",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 106 }
 , { "name" : "has_inv",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 325 }
 , { "name" : "has_lift_t",
 "topic" : "core",
 "file" : "core/init/coe.lean",
 "line" : 35 }
 , { "name" : "setoid",
 "topic" : "core",
 "file" : "core/init/data/setoid.lean",
 "line" : 10 }
 , { "name" : "left_cancel_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 101 }
 , { "name" : "monad_fail",
 "topic" : "core",
 "file" : "core/init/control/monad_fail.lean",
 "line" : 11 }
 , { "name" : "is_lawful_monad",
 "topic" : "core",
 "file" : "core/init/control/lawful.lean",
 "line" : 44 }
 , { "name" : "has_to_tactic_format",
 "topic" : "core",
 "file" : "core/init/meta/tactic.lean",
 "line" : 302 }
 , { "name" : "has_lt",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 332 }
 , { "name" : "is_right_null",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 31 }
 , { "name" : "semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 52 }
 , { "name" : "has_well_founded",
 "topic" : "core",
 "file" : "core/init/wf.lean",
 "line" : 27 }
 , { "name" : "fact",
 "topic" : "logic",
 "file" : "logic/basic.lean",
 "line" : 153 }
 , { "name" : "has_monad_lift_t",
 "topic" : "core",
 "file" : "core/init/control/lift.lean",
 "line" : 27 }
 , { "name" : "add_monoid",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 170 }
 , { "name" : "inhabited",
 "topic" : "core",
 "file" : "core/init/logic.lean",
 "line" : 770 }
 , { "name" : "is_right_distrib",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 46 }
 , { "name" : "has_orelse",
 "topic" : "core",
 "file" : "core/init/control/alternative.lean",
 "line" : 10 }
 , { "name" : "is_left_distrib",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 43 }
 , { "name" : "has_mem",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 351 }
 , { "name" : "is_incomp_trans",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 116 }
 , { "name" : "is_trichotomous",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 121 }
 , { "name" : "is_equiv",
 "topic" : "core",
 "file" : "core/init/algebra/classes.lean",
 "line" : 110 }
 , { "name" : "has_equiv",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 338 }
 , { "name" : "is_lawful_applicative",
 "topic" : "core",
 "file" : "core/init/control/lawful.lean",
 "line" : 26 }
 , { "name" : "has_sub",
 "topic" : "core",
 "file" : "core/init/core.lean",
 "line" : 327 }
 , { "name" : "monad_run",
 "topic" : "core",
 "file" : "core/init/control/lift.lean",
 "line" : 80 }
 , { "name" : "add_semigroup",
 "topic" : "algebra",
 "file" : "algebra/group/defs.lean",
 "line" : 55 }
 ]
 ,
  "edges" :

 [{ "name" : "widget.interactive_expression.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/widget/interactive_expr.lean",
 "line" : 37 }
 , { "name" : "prod.has_to_tactic_format",
 "topic" : "core",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 316 }
 , { "name" : "list.decidable_bex",
 "topic" : "core",
 "source" : "list",
 "target" : "decidable",
 "file" : "core/init/data/list/instances.lean",
 "line" : 36 }
 , { "name" : "reflected.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 327 }
 , { "name" : "group.to_has_inv",
 "topic" : "algebra",
 "source" : "group",
 "target" : "has_inv",
 "file" : "algebra/group/defs.lean",
 "line" : 226 }
 , { "name" : "int.decidable_lt",
 "topic" : "core",
 "source" : "int",
 "target" : "decidable",
 "file" : "core/init/data/int/order.lean",
 "line" : 28 }
 , { "name" : "interactive.loc.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "nat.has_mod",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mod",
 "file" : "core/init/data/nat/div.lean",
 "line" : 29 }
 , { "name" : "binder_info.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/expr.lean",
 "line" : 35 }
 , { "name" : "tactic_doc_entry.has_to_string",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "tactic/doc_commands.lean",
 "line" : 148 }
 , { "name" : "preorder.to_has_lt",
 "topic" : "core",
 "source" : "preorder",
 "target" : "has_lt",
 "file" : "core/init/algebra/order.lean",
 "line" : 19 }
 , { "name" : "name.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 127 }
 , { "name" : "module_info.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/module_info.lean",
 "line" : 48 }
 , { "name" : "binder.decidable_eq",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "meta/expr.lean",
 "line" : 181 }
 , { "name" : "option.has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 534 }
 , { "name" : "coe_base_aux",
 "topic" : "core",
 "source" : "has_coe",
 "target" : "has_coe_t_aux",
 "file" : "core/init/coe.lean",
 "line" : 129 }
 , { "name" : "tactic_state.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/tactic.lean",
 "line" : 38 }
 , { "name" : "punit.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/punit.lean",
 "line" : 21 }
 , { "name" : "add_left_cancel_monoid.to_add_monoid",
 "topic" : "algebra",
 "source" : "add_left_cancel_monoid",
 "target" : "add_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 218 }
 , { "name" : "array.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/data/array/basic.lean",
 "line" : 234 }
 , { "name" : "local_context.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/meta/local_context.lean",
 "line" : 55 }
 , { "name" : "prod.decidable_eq",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "decidable_eq",
 "file" : "core/init/data/prod.lean",
 "line" : 19 }
 , { "name" : "exists_prop_decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 723 }
 , { "name" : "fin.has_one",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_one",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 56 }
 , { "name" : "ite.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 956 }
 , { "name" : "tactic.apply_cfg.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "has_coe_t_aux.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 123 }
 , { "name" : "unsigned.has_mod",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mod",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 16 }
 , { "name" : "char.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/char/basic.lean",
 "line" : 70 }
 , { "name" : "widget_override.interactive_expression.has_repr",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "tactic/interactive_expr.lean",
 "line" : 51 }
 , { "name" : "tactic.interactive.rw_rule.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/interactive.lean",
 "line" : 330 }
 , { "name" : "list.decidable_ball",
 "topic" : "core",
 "source" : "list",
 "target" : "decidable",
 "file" : "core/init/data/list/instances.lean",
 "line" : 57 }
 , { "name" : "is_strict_weak_order_of_decidable_linear_order",
 "topic" : "core",
 "source" : "decidable_linear_order",
 "target" : "is_strict_weak_order",
 "file" : "core/init/algebra/order.lean",
 "line" : 238 }
 , { "name" : "tactic_doc_entry.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "smt_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 39 }
 , { "name" : "unsigned.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 19 }
 , { "name" : "alternative.to_applicative",
 "topic" : "core",
 "source" : "alternative",
 "target" : "applicative",
 "file" : "core/init/control/alternative.lean",
 "line" : 15 }
 , { "name" : "option.lift_or_get_comm",
 "topic" : "data",
 "source" : "is_commutative",
 "target" : "is_commutative",
 "file" : "data/option/defs.lean",
 "line" : 83 }
 , { "name" : "is_symm_op_of_is_symm",
 "topic" : "core",
 "source" : "is_symm",
 "target" : "is_symm_op",
 "file" : "core/init/algebra/classes.lean",
 "line" : 83 }
 , { "name" : "int.has_add",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_add",
 "file" : "core/init/data/int/basic.lean",
 "line" : 86 }
 , { "name" : "monad_reader_trans",
 "topic" : "core",
 "source" : "has_monad_lift",
 "target" : "monad_reader",
 "file" : "core/init/control/reader.lean",
 "line" : 88 }
 , { "name" : "nat.has_pow",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_pow",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 208 }
 , { "name" : "is_preorder.to_is_trans",
 "topic" : "core",
 "source" : "is_preorder",
 "target" : "is_trans",
 "file" : "core/init/algebra/classes.lean",
 "line" : 98 }
 , { "name" : "param_info.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 9 }
 , { "name" : "option.is_lawful_monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "core/init/data/option/instances.lean",
 "line" : 13 }
 , { "name" : "sigma.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 71 }
 , { "name" : "add_right_cancel_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 139 }
 , { "name" : "has_monad_lift_t_trans",
 "topic" : "core",
 "source" : "has_monad_lift",
 "target" : "has_monad_lift_t",
 "file" : "core/init/control/lift.lean",
 "line" : 37 }
 , { "name" : "option.has_to_tactic_format",
 "topic" : "core",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 324 }
 , { "name" : "name.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/meta/name.lean",
 "line" : 103 }
 , { "name" : "prod.has_reflect",
 "topic" : "core",
 "source" : "reflected",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "lean.parser.reflectable.optional",
 "topic" : "core",
 "source" : "lean.parser.reflectable",
 "target" : "lean.parser.reflectable",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 144 }
 , { "name" : "tactic.interactive.case_tag.match_result.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/case_tag.lean",
 "line" : 252 }
 , { "name" : "int.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/data/int/order.lean",
 "line" : 21 }
 , { "name" : "group.to_left_cancel_semigroup",
 "topic" : "algebra",
 "source" : "group",
 "target" : "left_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 267 }
 , { "name" : "interactive.loc.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "unsigned.has_zero",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_zero",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 11 }
 , { "name" : "congr_arg_kind.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/congr_lemma.lean",
 "line" : 29 }
 , { "name" : "sigma.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 150 }
 , { "name" : "monoid_to_is_left_id",
 "topic" : "algebra",
 "source" : "monoid",
 "target" : "is_left_id",
 "file" : "algebra/group/defs.lean",
 "line" : 188 }
 , { "name" : "pos.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "option.lift_or_get_idem",
 "topic" : "data",
 "source" : "is_idempotent",
 "target" : "is_idempotent",
 "file" : "data/option/defs.lean",
 "line" : 91 }
 , { "name" : "local_context.decidable",
 "topic" : "core",
 "source" : "local_context",
 "target" : "decidable",
 "file" : "core/init/meta/local_context.lean",
 "line" : 58 }
 , { "name" : "has_orelse.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/alternative.lean",
 "line" : 10 }
 , { "name" : "char.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 53 }
 , { "name" : "unsigned.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/unsigned/basic.lean",
 "line" : 28 }
 , { "name" : "array.decidable_eq",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "decidable_eq",
 "file" : "core/init/data/array/basic.lean",
 "line" : 264 }
 , { "name" : "int.has_div",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_div",
 "file" : "core/init/data/int/basic.lean",
 "line" : 314 }
 , { "name" : "tactic.rewrite_cfg.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/rewrite_tactic.lean",
 "line" : 11 }
 , { "name" : "conv.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/converter/conv.lean",
 "line" : 22 }
 , { "name" : "has_bind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/monad.lean",
 "line" : 12 }
 , { "name" : "ne.decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 734 }
 , { "name" : "expr.has_to_string",
 "topic" : "core",
 "source" : "bool",
 "target" : "has_to_string",
 "file" : "core/init/meta/expr.lean",
 "line" : 143 }
 , { "name" : "string_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/format.lean",
 "line" : 82 }
 , { "name" : "_private.1627920919.fun_setoid",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "setoid",
 "file" : "core/init/funext.lean",
 "line" : 37 }
 , { "name" : "nat.decidable_linear_order",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_linear_order",
 "file" : "core/init/data/nat/lemmas.lean",
 "line" : 297 }
 , { "name" : "option_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/option.lean",
 "line" : 11 }
 , { "name" : "add_monoid_to_is_right_id",
 "topic" : "algebra",
 "source" : "add_monoid",
 "target" : "is_right_id",
 "file" : "algebra/group/defs.lean",
 "line" : 192 }
 , { "name" : "expr.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/expr.lean",
 "line" : 134 }
 , { "name" : "add_comm_group.to_add_comm_monoid",
 "topic" : "algebra",
 "source" : "add_comm_group",
 "target" : "add_comm_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 301 }
 , { "name" : "empty.decidable_eq",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "logic/basic.lean",
 "line" : 38 }
 , { "name" : "sum_has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 138 }
 , { "name" : "subtype.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 74 }
 , { "name" : "option_t.monad_run",
 "topic" : "core",
 "source" : "monad_run",
 "target" : "monad_run",
 "file" : "core/init/control/option.lean",
 "line" : 64 }
 , { "name" : "doc_category.has_to_format",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "tactic/doc_commands.lean",
 "line" : 129 }
 , { "name" : "smt_pre_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "doc_category.has_sizeof_inst",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "tactic/doc_commands.lean",
 "line" : 119 }
 , { "name" : "hinst_lemma.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/smt/ematch.lean",
 "line" : 25 }
 , { "name" : "name.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/meta/name.lean",
 "line" : 98 }
 , { "name" : "has_coe.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 38 }
 , { "name" : "reducibility_hints.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "add_group.to_has_neg",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "has_neg",
 "file" : "algebra/group/defs.lean",
 "line" : 230 }
 , { "name" : "unsigned.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 18 }
 , { "name" : "conv.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/meta/converter/conv.lean",
 "line" : 28 }
 , { "name" : "monad_reader_adapter_trans",
 "topic" : "core",
 "source" : "monad_reader_adapter",
 "target" : "monad_reader_adapter",
 "file" : "core/init/control/reader.lean",
 "line" : 113 }
 , { "name" : "coe_to_lift",
 "topic" : "core",
 "source" : "has_coe_t",
 "target" : "has_lift_t",
 "file" : "core/init/coe.lean",
 "line" : 142 }
 , { "name" : "has_coe_to_fun.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 45 }
 , { "name" : "expr.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/expr.lean",
 "line" : 114 }
 , { "name" : "conv.monad_fail",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_fail",
 "file" : "core/init/meta/converter/conv.lean",
 "line" : 25 }
 , { "name" : "list.has_subset",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_subset",
 "file" : "core/init/data/list/lemmas.lean",
 "line" : 143 }
 , { "name" : "list.has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 541 }
 , { "name" : "string.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 25 }
 , { "name" : "local_context.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/local_context.lean",
 "line" : 45 }
 , { "name" : "add_comm_monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 207 }
 , { "name" : "comm_group.to_group",
 "topic" : "algebra",
 "source" : "comm_group",
 "target" : "group",
 "file" : "algebra/group/defs.lean",
 "line" : 298 }
 , { "name" : "int.has_zero",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_zero",
 "file" : "core/init/data/int/basic.lean",
 "line" : 42 }
 , { "name" : "int.has_sub",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sub",
 "file" : "core/init/data/int/basic.lean",
 "line" : 93 }
 , { "name" : "monad_except_adapter.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/except.lean",
 "line" : 129 }
 , { "name" : "is_strict_total_order.to_is_strict_weak_order",
 "topic" : "core",
 "source" : "is_strict_total_order",
 "target" : "is_strict_weak_order",
 "file" : "core/init/algebra/classes.lean",
 "line" : 124 }
 , { "name" : "is_asymm_of_is_trans_of_is_irrefl",
 "topic" : "core",
 "source" : "is_irrefl",
 "target" : "is_asymm",
 "file" : "core/init/algebra/classes.lean",
 "line" : 158 }
 , { "name" : "occurrences.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/occurrences.lean",
 "line" : 21 }
 , { "name" : "name.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/name.lean",
 "line" : 25 }
 , { "name" : "environment.projection_info.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "fin.has_sub",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_sub",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 58 }
 , { "name" : "rbmap.inhabited",
 "topic" : "tactic",
 "source" : "auto_param",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 76 }
 , { "name" : "add_group.to_add_left_cancel_monoid",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "add_left_cancel_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 291 }
 , { "name" : "dite.decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 962 }
 , { "name" : "tactic.unfold_proj_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "name_set.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/rb_map.lean",
 "line" : 202 }
 , { "name" : "is_strict_weak_order.to_is_incomp_trans",
 "topic" : "core",
 "source" : "is_strict_weak_order",
 "target" : "is_incomp_trans",
 "file" : "core/init/algebra/classes.lean",
 "line" : 119 }
 , { "name" : "char.decidable_lt",
 "topic" : "core",
 "source" : "char",
 "target" : "decidable",
 "file" : "core/init/data/char/basic.lean",
 "line" : 34 }
 , { "name" : "monad_reader_adapter.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/reader.lean",
 "line" : 106 }
 , { "name" : "native.rb_map.has_to_tactic_format",
 "topic" : "meta",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "meta/rb_map.lean",
 "line" : 131 }
 , { "name" : "tactic.dsimp_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 125 }
 , { "name" : "bin_tree.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 69 }
 , { "name" : "bool.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/logic.lean",
 "line" : 744 }
 , { "name" : "native.float.has_one",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_one",
 "file" : "core/init/meta/float.lean",
 "line" : 144 }
 , { "name" : "monad.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/monad.lean",
 "line" : 23 }
 , { "name" : "nat.has_mul",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mul",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 41 }
 , { "name" : "reader_t.monad_except",
 "topic" : "core",
 "source" : "monad_except",
 "target" : "monad_except",
 "file" : "core/init/control/reader.lean",
 "line" : 66 }
 , { "name" : "is_partial_order.to_is_preorder",
 "topic" : "core",
 "source" : "is_partial_order",
 "target" : "is_preorder",
 "file" : "core/init/algebra/classes.lean",
 "line" : 106 }
 , { "name" : "sum.is_lawful_monad",
 "topic" : "control",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "control/basic.lean",
 "line" : 185 }
 , { "name" : "punit.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 523 }
 , { "name" : "subtype.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 156 }
 , { "name" : "vm_obj_kind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/vm.lean",
 "line" : 13 }
 , { "name" : "add_group.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 230 }
 , { "name" : "fin.has_lt",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_lt",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 21 }
 , { "name" : "list.decidable_mem",
 "topic" : "core",
 "source" : "list",
 "target" : "decidable",
 "file" : "core/init/data/list/basic.lean",
 "line" : 50 }
 , { "name" : "name_map.inhabited",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "meta/rb_map.lean",
 "line" : 199 }
 , { "name" : "array.has_to_tactic_format",
 "topic" : "core",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "core/init/data/array/basic.lean",
 "line" : 237 }
 , { "name" : "is_partial_order.to_is_antisymm",
 "topic" : "core",
 "source" : "is_partial_order",
 "target" : "is_antisymm",
 "file" : "core/init/algebra/classes.lean",
 "line" : 106 }
 , { "name" : "vm_decl_kind.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "vm_obj_kind.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/vm.lean",
 "line" : 13 }
 , { "name" : "fin.has_le",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_le",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 22 }
 , { "name" : "ordering.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/ordering/basic.lean",
 "line" : 11 }
 , { "name" : "environment.projection_info.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/environment.lean",
 "line" : 39 }
 , { "name" : "add_monoid.to_add_semigroup",
 "topic" : "algebra",
 "source" : "add_monoid",
 "target" : "add_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 170 }
 , { "name" : "subsingleton_info.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 85 }
 , { "name" : "set.has_sep",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sep",
 "file" : "core/init/data/set.lean",
 "line" : 34 }
 , { "name" : "to_additive.value_type.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/to_additive.lean",
 "line" : 81 }
 , { "name" : "native.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/meta/rb_map.lean",
 "line" : 106 }
 , { "name" : "native.float.has_add",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_add",
 "file" : "core/init/meta/float.lean",
 "line" : 61 }
 , { "name" : "array.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/array/basic.lean",
 "line" : 231 }
 , { "name" : "has_le.le.is_total_preorder",
 "topic" : "core",
 "source" : "decidable_linear_order",
 "target" : "is_total_preorder",
 "file" : "core/init/algebra/order.lean",
 "line" : 234 }
 , { "name" : "state_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/state.lean",
 "line" : 13 }
 , { "name" : "rbtree.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/rbtree/basic.lean",
 "line" : 197 }
 , { "name" : "option.lift_or_get_is_left_id",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "is_left_id",
 "file" : "data/option/defs.lean",
 "line" : 95 }
 , { "name" : "list.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/data/list/instances.lean",
 "line" : 24 }
 , { "name" : "binder_info.inhabited",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "meta/expr.lean",
 "line" : 26 }
 , { "name" : "implies.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 701 }
 , { "name" : "tactic_doc_entry.has_reflect",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "tactic/doc_commands.lean",
 "line" : 133 }
 , { "name" : "add_group.to_left_cancel_add_semigroup",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "add_left_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 267 }
 , { "name" : "has_lift_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 35 }
 , { "name" : "plift.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/logic.lean",
 "line" : 993 }
 , { "name" : "left_cancel_monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 212 }
 , { "name" : "sum.inhabited_left",
 "topic" : "core",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "core/init/data/sum/basic.lean",
 "line" : 17 }
 , { "name" : "smt_tactic.monad_fail",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_fail",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 79 }
 , { "name" : "expr.decidable_rel",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/meta/expr.lean",
 "line" : 289 }
 , { "name" : "quotient.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/quot.lean",
 "line" : 261 }
 , { "name" : "string.iterator_imp.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/string/basic.lean",
 "line" : 66 }
 , { "name" : "lift_fn",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 170 }
 , { "name" : "unsigned.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 59 }
 , { "name" : "list.reflect",
 "topic" : "core",
 "source" : "reflected",
 "target" : "has_reflect",
 "file" : "core/init/meta/has_reflect.lean",
 "line" : 50 }
 , { "name" : "not.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 698 }
 , { "name" : "expr.coord.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 46 }
 , { "name" : "char.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/data/char/basic.lean",
 "line" : 32 }
 , { "name" : "task.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/tactic.lean",
 "line" : 1743 }
 , { "name" : "bool.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "int.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/int/basic.lean",
 "line" : 29 }
 , { "name" : "unsigned.has_mul",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mul",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 15 }
 , { "name" : "monad.to_has_bind",
 "topic" : "core",
 "source" : "monad",
 "target" : "has_bind",
 "file" : "core/init/control/monad.lean",
 "line" : 23 }
 , { "name" : "xor.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 715 }
 , { "name" : "native.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/rb_map.lean",
 "line" : 96 }
 , { "name" : "is_strict_weak_order.to_is_strict_order",
 "topic" : "core",
 "source" : "is_strict_weak_order",
 "target" : "is_strict_order",
 "file" : "core/init/algebra/classes.lean",
 "line" : 119 }
 , { "name" : "module_info.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/module_info.lean",
 "line" : 51 }
 , { "name" : "tactic.tactic.has_to_tactic_format",
 "topic" : "tactic",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "tactic/core.lean",
 "line" : 1862 }
 , { "name" : "set.has_subset",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_subset",
 "file" : "core/init/data/set.lean",
 "line" : 28 }
 , { "name" : "coe_sort_bool",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe_to_sort",
 "file" : "core/init/coe.lean",
 "line" : 155 }
 , { "name" : "rbmap.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/rbmap/basic.lean",
 "line" : 60 }
 , { "name" : "monad_state_adapter_trans",
 "topic" : "core",
 "source" : "monad_state_adapter",
 "target" : "monad_state_adapter",
 "file" : "core/init/control/state.lean",
 "line" : 166 }
 , { "name" : "list.has_sdiff",
 "topic" : "data",
 "source" : "decidable_eq",
 "target" : "has_sdiff",
 "file" : "data/list/defs.lean",
 "line" : 23 }
 , { "name" : "reader_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/reader.lean",
 "line" : 14 }
 , { "name" : "rsimp.config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "has_to_string.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/to_string.lean",
 "line" : 19 }
 , { "name" : "prod_has_decidable_lt",
 "topic" : "core",
 "source" : "prod",
 "target" : "decidable",
 "file" : "core/init/data/prod.lean",
 "line" : 33 }
 , { "name" : "lift_pair₁",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 182 }
 , { "name" : "bool.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/logic.lean",
 "line" : 784 }
 , { "name" : "to_additive.value_type.has_reflect",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "algebra/group/to_additive.lean",
 "line" : 81 }
 , { "name" : "nat.has_zero",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_zero",
 "file" : "core/init/core.lean",
 "line" : 425 }
 , { "name" : "psigma.has_well_founded",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_well_founded",
 "file" : "core/init/data/sigma/lex.lean",
 "line" : 118 }
 , { "name" : "sum.has_reflect",
 "topic" : "core",
 "source" : "reflected",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "monad_except.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/except.lean",
 "line" : 99 }
 , { "name" : "environment.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/environment.lean",
 "line" : 210 }
 , { "name" : "tactic.dunfold_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 199 }
 , { "name" : "smt_state.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 59 }
 , { "name" : "sigma.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 511 }
 , { "name" : "comm_monoid.to_comm_semigroup",
 "topic" : "algebra",
 "source" : "comm_monoid",
 "target" : "comm_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 203 }
 , { "name" : "nat.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 50 }
 , { "name" : "unsigned.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 149 }
 , { "name" : "has_seq.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/applicative.lean",
 "line" : 16 }
 , { "name" : "add_comm_monoid.to_add_monoid",
 "topic" : "algebra",
 "source" : "add_comm_monoid",
 "target" : "add_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 207 }
 , { "name" : "ordering.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/ordering/basic.lean",
 "line" : 42 }
 , { "name" : "expr.has_to_format",
 "topic" : "core",
 "source" : "bool",
 "target" : "has_to_format",
 "file" : "core/init/meta/expr.lean",
 "line" : 144 }
 , { "name" : "add_comm_group.to_add_group",
 "topic" : "algebra",
 "source" : "add_comm_group",
 "target" : "add_group",
 "file" : "algebra/group/defs.lean",
 "line" : 301 }
 , { "name" : "tactic.interactive.case_tag.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/case_tag.lean",
 "line" : 166 }
 , { "name" : "has_coe_to_sort.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 48 }
 , { "name" : "sum.monad",
 "topic" : "control",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "control/basic.lean",
 "line" : 178 }
 , { "name" : "option.has_mem",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "data/option/defs.lean",
 "line" : 19 }
 , { "name" : "ulift.inhabited",
 "topic" : "tactic",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "widget.html.has_emptyc",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_emptyc",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 287 }
 , { "name" : "has_pure.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/applicative.lean",
 "line" : 11 }
 , { "name" : "exceptional.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/meta/exceptional.lean",
 "line" : 26 }
 , { "name" : "tactic.unsafe.type_context.monad_fail",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_fail",
 "file" : "core/init/meta/type_context.lean",
 "line" : 17 }
 , { "name" : "reader_t.is_lawful_monad",
 "topic" : "core",
 "source" : "is_lawful_monad",
 "target" : "is_lawful_monad",
 "file" : "core/init/control/lawful.lean",
 "line" : 201 }
 , { "name" : "native.float.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/float.lean",
 "line" : 148 }
 , { "name" : "reflected.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/expr.lean",
 "line" : 280 }
 , { "name" : "nat.linear_order",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "linear_order",
 "file" : "core/init/data/nat/lemmas.lean",
 "line" : 171 }
 , { "name" : "set.functor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "functor",
 "file" : "core/init/data/set.lean",
 "line" : 86 }
 , { "name" : "string.has_reflect",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "tactic/fix_reflect_string.lean",
 "line" : 36 }
 , { "name" : "state_t.monad_except",
 "topic" : "core",
 "source" : "monad_except",
 "target" : "monad_except",
 "file" : "core/init/control/state.lean",
 "line" : 75 }
 , { "name" : "punit.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/punit.lean",
 "line" : 18 }
 , { "name" : "right_cancel_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 133 }
 , { "name" : "occurrences.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/occurrences.lean",
 "line" : 41 }
 , { "name" : "is_preorder.to_is_refl",
 "topic" : "core",
 "source" : "is_preorder",
 "target" : "is_refl",
 "file" : "core/init/algebra/classes.lean",
 "line" : 98 }
 , { "name" : "tactic.interactive.case_tag.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/case_tag.lean",
 "line" : 169 }
 , { "name" : "option.decidable_exists_mem",
 "topic" : "data",
 "source" : "option",
 "target" : "decidable",
 "file" : "data/option/defs.lean",
 "line" : 46 }
 , { "name" : "is_comm_applicative.to_is_lawful_applicative",
 "topic" : "control",
 "source" : "is_comm_applicative",
 "target" : "is_lawful_applicative",
 "file" : "control/basic.lean",
 "line" : 195 }
 , { "name" : "except.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/control/except.lean",
 "line" : 46 }
 , { "name" : "local_context.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/local_context.lean",
 "line" : 35 }
 , { "name" : "string.reflect",
 "topic" : "core",
 "source" : "string",
 "target" : "reflected",
 "file" : "core/init/meta/expr.lean",
 "line" : 273 }
 , { "name" : "add_monoid_to_is_left_id",
 "topic" : "algebra",
 "source" : "add_monoid",
 "target" : "is_left_id",
 "file" : "algebra/group/defs.lean",
 "line" : 188 }
 , { "name" : "sum.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 65 }
 , { "name" : "environment.implicit_infer_kind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/environment.lean",
 "line" : 54 }
 , { "name" : "rbnode.color.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/rbtree/basic.lean",
 "line" : 24 }
 , { "name" : "add_semigroup.to_is_associative",
 "topic" : "algebra",
 "source" : "add_semigroup",
 "target" : "is_associative",
 "file" : "algebra/group/defs.lean",
 "line" : 69 }
 , { "name" : "reader_t.monad_reader_adapter",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_reader_adapter",
 "file" : "core/init/control/reader.lean",
 "line" : 116 }
 , { "name" : "tactic.simp_arg_type.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/interactive.lean",
 "line" : 1065 }
 , { "name" : "fun_info.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 50 }
 , { "name" : "string.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/string/basic.lean",
 "line" : 143 }
 , { "name" : "tactic.simp_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "format.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/format.lean",
 "line" : 58 }
 , { "name" : "add_comm_semigroup.to_add_semigroup",
 "topic" : "algebra",
 "source" : "add_comm_semigroup",
 "target" : "add_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 81 }
 , { "name" : "pi.subsingleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "core/init/funext.lean",
 "line" : 60 }
 , { "name" : "true.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/logic.lean",
 "line" : 786 }
 , { "name" : "has_le.le.decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/algebra/order.lean",
 "line" : 224 }
 , { "name" : "fin.has_add",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_add",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 57 }
 , { "name" : "add_group_has_sub",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "has_sub",
 "file" : "algebra/group/defs.lean",
 "line" : 285 }
 , { "name" : "level.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/level.lean",
 "line" : 42 }
 , { "name" : "has_seq_right.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/applicative.lean",
 "line" : 26 }
 , { "name" : "ordering.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/ordering/basic.lean",
 "line" : 14 }
 , { "name" : "semigroup.to_has_mul",
 "topic" : "algebra",
 "source" : "semigroup",
 "target" : "has_mul",
 "file" : "algebra/group/defs.lean",
 "line" : 52 }
 , { "name" : "psum.inhabited_right",
 "topic" : "logic",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "logic/basic.lean",
 "line" : 44 }
 , { "name" : "linear_order.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/algebra/order.lean",
 "line" : 30 }
 , { "name" : "nat.has_add",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_add",
 "file" : "core/init/core.lean",
 "line" : 429 }
 , { "name" : "left_cancel_monoid.to_left_cancel_semigroup",
 "topic" : "algebra",
 "source" : "left_cancel_monoid",
 "target" : "left_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 212 }
 , { "name" : "local_context.has_emptyc",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_emptyc",
 "file" : "core/init/meta/local_context.lean",
 "line" : 51 }
 , { "name" : "pos.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/expr.lean",
 "line" : 15 }
 , { "name" : "smt_tactic.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 65 }
 , { "name" : "int.has_mul",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mul",
 "file" : "core/init/data/int/basic.lean",
 "line" : 87 }
 , { "name" : "expr.address.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 77 }
 , { "name" : "tactic.goal.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/core.lean",
 "line" : 1780 }
 , { "name" : "tactic.transparency.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "string.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/string/basic.lean",
 "line" : 146 }
 , { "name" : "string_to_name",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/name.lean",
 "line" : 37 }
 , { "name" : "local_context.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/meta/local_context.lean",
 "line" : 47 }
 , { "name" : "nat.has_dvd",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_dvd",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 45 }
 , { "name" : "decidable_lt_of_decidable_le",
 "topic" : "core",
 "source" : "decidable_rel",
 "target" : "decidable_rel",
 "file" : "core/init/algebra/order.lean",
 "line" : 191 }
 , { "name" : "list.decidable_chain",
 "topic" : "data",
 "source" : "list",
 "target" : "decidable",
 "file" : "data/list/defs.lean",
 "line" : 437 }
 , { "name" : "lift_pair",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 179 }
 , { "name" : "sum.inhabited_right",
 "topic" : "core",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "core/init/data/sum/basic.lean",
 "line" : 20 }
 , { "name" : "nat.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 23 }
 , { "name" : "monad_functor.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/lift.lean",
 "line" : 50 }
 , { "name" : "widget_override.interactive_expression.has_to_string",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "tactic/interactive_expr.lean",
 "line" : 50 }
 , { "name" : "rbnode.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/data/rbtree/basic.lean",
 "line" : 11 }
 , { "name" : "binder_info.has_reflect",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "meta/expr.lean",
 "line" : null }
 , { "name" : "char.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 115 }
 , { "name" : "options.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 97 }
 , { "name" : "char.decidable_is_digit",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 48 }
 , { "name" : "rbmap.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/data/rbmap/basic.lean",
 "line" : 57 }
 , { "name" : "format.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 73 }
 , { "name" : "except.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/control/except.lean",
 "line" : 13 }
 , { "name" : "lift_trans",
 "topic" : "core",
 "source" : "has_lift",
 "target" : "has_lift_t",
 "file" : "core/init/coe.lean",
 "line" : 89 }
 , { "name" : "int.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/int/basic.lean",
 "line" : 15 }
 , { "name" : "to_additive.value_type.inhabited",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "algebra/group/to_additive.lean",
 "line" : 81 }
 , { "name" : "subtype.decidable_eq",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "decidable_eq",
 "file" : "core/init/data/subtype/instances.lean",
 "line" : 11 }
 , { "name" : "smt_tactic.has_andthen",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_andthen",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 250 }
 , { "name" : "alternative.to_has_orelse",
 "topic" : "core",
 "source" : "alternative",
 "target" : "has_orelse",
 "file" : "core/init/control/alternative.lean",
 "line" : 15 }
 , { "name" : "has_lt.lt.decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/algebra/order.lean",
 "line" : 221 }
 , { "name" : "tactic.rewrite_cfg.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "expr.coord.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 39 }
 , { "name" : "reader_t.monad_reader",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_reader",
 "file" : "core/init/control/reader.lean",
 "line" : 92 }
 , { "name" : "set.has_emptyc",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_emptyc",
 "file" : "core/init/data/set.lean",
 "line" : 37 }
 , { "name" : "state_t.alternative",
 "topic" : "core",
 "source" : "alternative",
 "target" : "alternative",
 "file" : "core/init/control/state.lean",
 "line" : 43 }
 , { "name" : "is_strict_order.to_is_irrefl",
 "topic" : "core",
 "source" : "is_strict_order",
 "target" : "is_irrefl",
 "file" : "core/init/algebra/classes.lean",
 "line" : 114 }
 , { "name" : "int.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/data/int/order.lean",
 "line" : 17 }
 , { "name" : "applicative.to_has_seq_right",
 "topic" : "core",
 "source" : "applicative",
 "target" : "has_seq_right",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "prod.inhabited",
 "topic" : "core",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "core/init/data/prod.lean",
 "line" : 16 }
 , { "name" : "monoid.to_has_one",
 "topic" : "algebra",
 "source" : "monoid",
 "target" : "has_one",
 "file" : "algebra/group/defs.lean",
 "line" : 166 }
 , { "name" : "decidable.subsingleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "core/init/logic.lean",
 "line" : 814 }
 , { "name" : "int.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/int/basic.lean",
 "line" : 32 }
 , { "name" : "add_semigroup.to_has_add",
 "topic" : "algebra",
 "source" : "add_semigroup",
 "target" : "has_add",
 "file" : "algebra/group/defs.lean",
 "line" : 55 }
 , { "name" : "char.decidable_is_punctuation",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 54 }
 , { "name" : "tactic.new_goals.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "char.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/char/basic.lean",
 "line" : 24 }
 , { "name" : "comm_monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 203 }
 , { "name" : "monad_functor_t_trans",
 "topic" : "core",
 "source" : "monad_functor",
 "target" : "monad_functor_t",
 "file" : "core/init/control/lift.lean",
 "line" : 61 }
 , { "name" : "prod.nonempty",
 "topic" : "logic",
 "source" : "nonempty",
 "target" : "nonempty",
 "file" : "logic/basic.lean",
 "line" : 967 }
 , { "name" : "is_linear_order.to_is_partial_order",
 "topic" : "core",
 "source" : "is_linear_order",
 "target" : "is_partial_order",
 "file" : "core/init/algebra/classes.lean",
 "line" : 108 }
 , { "name" : "list.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 122 }
 , { "name" : "tactic.transparency.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/tactic.lean",
 "line" : 370 }
 , { "name" : "tactic.unfold_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/interactive.lean",
 "line" : 1465 }
 , { "name" : "nat.decidable_lt",
 "topic" : "core",
 "source" : "nat",
 "target" : "decidable",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 110 }
 , { "name" : "expr.coord.has_dec_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 43 }
 , { "name" : "option_t.alternative",
 "topic" : "core",
 "source" : "monad",
 "target" : "alternative",
 "file" : "core/init/control/option.lean",
 "line" : 40 }
 , { "name" : "decidable.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 103 }
 , { "name" : "nat.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 485 }
 , { "name" : "decidable_eq_of_decidable_le",
 "topic" : "core",
 "source" : "decidable_rel",
 "target" : "decidable_eq",
 "file" : "core/init/algebra/order.lean",
 "line" : 203 }
 , { "name" : "format.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/meta/format.lean",
 "line" : 61 }
 , { "name" : "prod.has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 491 }
 , { "name" : "vm_decl_kind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/vm.lean",
 "line" : 49 }
 , { "name" : "is_strict_total_order_of_decidable_linear_order",
 "topic" : "core",
 "source" : "decidable_linear_order",
 "target" : "is_strict_total_order",
 "file" : "core/init/algebra/order.lean",
 "line" : 242 }
 , { "name" : "group.to_right_cancel_semigroup",
 "topic" : "algebra",
 "source" : "group",
 "target" : "right_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 272 }
 , { "name" : "int.has_one",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_one",
 "file" : "core/init/data/int/basic.lean",
 "line" : 43 }
 , { "name" : "int.has_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/data/int/basic.lean",
 "line" : 21 }
 , { "name" : "tactic.opt_to_tac",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/tactic.lean",
 "line" : 251 }
 , { "name" : "reflected.has_to_pexpr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_pexpr",
 "file" : "core/init/meta/pexpr.lean",
 "line" : 45 }
 , { "name" : "name_set.inhabited",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "meta/rb_map.lean",
 "line" : 165 }
 , { "name" : "rbnode.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 74 }
 , { "name" : "expr.coord.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 18 }
 , { "name" : "local_context.decidable_rel",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/meta/local_context.lean",
 "line" : 49 }
 , { "name" : "set.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/data/set.lean",
 "line" : 22 }
 , { "name" : "binder.has_to_string",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "meta/expr.lean",
 "line" : 193 }
 , { "name" : "unsigned.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 71 }
 , { "name" : "subtype.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/subtype/basic.lean",
 "line" : 32 }
 , { "name" : "fin.has_sizeof_inst",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_sizeof",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 9 }
 , { "name" : "widget_override.local_collection.decidable_eq",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "tactic/interactive_expr.lean",
 "line" : 227 }
 , { "name" : "list.has_emptyc",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_emptyc",
 "file" : "core/init/data/list/basic.lean",
 "line" : 59 }
 , { "name" : "occurrences.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/occurrences.lean",
 "line" : 49 }
 , { "name" : "reducibility_hints.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/declaration.lean",
 "line" : 41 }
 , { "name" : "name.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/name.lean",
 "line" : 10 }
 , { "name" : "is_equiv.to_is_symm",
 "topic" : "core",
 "source" : "is_equiv",
 "target" : "is_symm",
 "file" : "core/init/algebra/classes.lean",
 "line" : 110 }
 , { "name" : "subsingleton_prop",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "core/init/logic.lean",
 "line" : 811 }
 , { "name" : "list.has_singleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_singleton",
 "file" : "core/init/data/list/basic.lean",
 "line" : 232 }
 , { "name" : "pexpr.decidable_eq",
 "topic" : "meta",
 "source" : "opt_param",
 "target" : "decidable_eq",
 "file" : "meta/expr.lean",
 "line" : 811 }
 , { "name" : "char.decidable_is_upper",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 39 }
 , { "name" : "nat.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 62 }
 , { "name" : "nat.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 48 }
 , { "name" : "expr.coord.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 40 }
 , { "name" : "list.decidable_chain'",
 "topic" : "data",
 "source" : "list",
 "target" : "decidable",
 "file" : "data/list/defs.lean",
 "line" : 440 }
 , { "name" : "bin_tree.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 570 }
 , { "name" : "format.color.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "native.float.of_int_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/float.lean",
 "line" : 140 }
 , { "name" : "set.has_sdiff",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sdiff",
 "file" : "core/init/data/set.lean",
 "line" : 72 }
 , { "name" : "tactic.unsafe.type_context.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/type_context.lean",
 "line" : 16 }
 , { "name" : "coe_sort_trans",
 "topic" : "core",
 "source" : "has_coe_t_aux",
 "target" : "has_coe_to_sort",
 "file" : "core/init/coe.lean",
 "line" : 136 }
 , { "name" : "thunk.has_reflect",
 "topic" : "tactic",
 "source" : "has_reflect",
 "target" : "has_reflect",
 "file" : "tactic/fix_reflect_string.lean",
 "line" : 31 }
 , { "name" : "string_imp.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/string/basic.lean",
 "line" : 15 }
 , { "name" : "expr.address.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 80 }
 , { "name" : "nat.decidable_le",
 "topic" : "core",
 "source" : "nat",
 "target" : "decidable",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 101 }
 , { "name" : "subtype.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 547 }
 , { "name" : "coe_decidable_eq",
 "topic" : "core",
 "source" : "bool",
 "target" : "decidable",
 "file" : "core/init/coe.lean",
 "line" : 158 }
 , { "name" : "option_t.monad_functor",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_functor",
 "file" : "core/init/control/option.lean",
 "line" : 54 }
 , { "name" : "add_comm_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 81 }
 , { "name" : "linear_order.to_partial_order",
 "topic" : "core",
 "source" : "linear_order",
 "target" : "partial_order",
 "file" : "core/init/algebra/order.lean",
 "line" : 30 }
 , { "name" : "has_lift.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 31 }
 , { "name" : "monad.to_applicative",
 "topic" : "core",
 "source" : "monad",
 "target" : "applicative",
 "file" : "core/init/control/monad.lean",
 "line" : 23 }
 , { "name" : "interaction_monad.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/interaction_monad.lean",
 "line" : 70 }
 , { "name" : "subsingleton_pempty",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "logic/basic.lean",
 "line" : 105 }
 , { "name" : "pos.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/expr.lean",
 "line" : 11 }
 , { "name" : "id.is_lawful_monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "core/init/control/lawful.lean",
 "line" : 84 }
 , { "name" : "prod.has_lt",
 "topic" : "core",
 "source" : "has_lt",
 "target" : "has_lt",
 "file" : "core/init/data/prod.lean",
 "line" : 30 }
 , { "name" : "native.rb_set.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/rb_map.lean",
 "line" : 170 }
 , { "name" : "tactic.interactive.rw_rules_t.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/interactive.lean",
 "line" : 376 }
 , { "name" : "has_repr.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/repr.lean",
 "line" : 29 }
 , { "name" : "nonempty_of_inhabited",
 "topic" : "core",
 "source" : "inhabited",
 "target" : "nonempty",
 "file" : "core/init/logic.lean",
 "line" : 794 }
 , { "name" : "list.has_decidable_le",
 "topic" : "core",
 "source" : "list",
 "target" : "decidable",
 "file" : "core/init/data/list/basic.lean",
 "line" : 333 }
 , { "name" : "fin.has_repr",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 146 }
 , { "name" : "monad_fail_lift",
 "topic" : "core",
 "source" : "has_monad_lift",
 "target" : "monad_fail",
 "file" : "core/init/control/monad_fail.lean",
 "line" : 17 }
 , { "name" : "widget.attr.is_functor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "functor",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 276 }
 , { "name" : "fin.decidable_lt",
 "topic" : "core",
 "source" : "fin",
 "target" : "decidable",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 24 }
 , { "name" : "functor.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/functor.lean",
 "line" : 11 }
 , { "name" : "tactic.new_goals.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/tactic.lean",
 "line" : 521 }
 , { "name" : "widget.tc.cfn",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe_to_fun",
 "file" : "core/init/meta/widget/tactic_component.lean",
 "line" : 83 }
 , { "name" : "is_strict_order.to_is_trans",
 "topic" : "core",
 "source" : "is_strict_order",
 "target" : "is_trans",
 "file" : "core/init/algebra/classes.lean",
 "line" : 114 }
 , { "name" : "name.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/name.lean",
 "line" : 85 }
 , { "name" : "expr.reflect",
 "topic" : "core",
 "source" : "expr",
 "target" : "reflected",
 "file" : "core/init/meta/expr.lean",
 "line" : 272 }
 , { "name" : "tactic.delta_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "partial_order.to_preorder",
 "topic" : "core",
 "source" : "partial_order",
 "target" : "preorder",
 "file" : "core/init/algebra/order.lean",
 "line" : 26 }
 , { "name" : "state_t.monad_state_adapter",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_state_adapter",
 "file" : "core/init/control/state.lean",
 "line" : 169 }
 , { "name" : "add_monoid.to_has_zero",
 "topic" : "algebra",
 "source" : "add_monoid",
 "target" : "has_zero",
 "file" : "algebra/group/defs.lean",
 "line" : 170 }
 , { "name" : "bool.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 28 }
 , { "name" : "tactic.simp_arg_type_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/interactive.lean",
 "line" : 1071 }
 , { "name" : "applicative.to_functor",
 "topic" : "core",
 "source" : "applicative",
 "target" : "functor",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "subsingleton_info.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "decidable.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 31 }
 , { "name" : "unsigned.has_one",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_one",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 12 }
 , { "name" : "set.is_lawful_singleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_singleton",
 "file" : "core/init/data/set.lean",
 "line" : 51 }
 , { "name" : "rbnode.color.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "reader_t.has_monad_lift",
 "topic" : "core",
 "source" : "monad",
 "target" : "has_monad_lift",
 "file" : "core/init/control/reader.lean",
 "line" : 44 }
 , { "name" : "native.float.has_zero",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_zero",
 "file" : "core/init/meta/float.lean",
 "line" : 143 }
 , { "name" : "widget.mouse_event_kind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 169 }
 , { "name" : "expr.address.has_dec_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 70 }
 , { "name" : "list.bin_tree_to_list",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/data/list/instances.lean",
 "line" : 33 }
 , { "name" : "is_per.to_is_symm",
 "topic" : "core",
 "source" : "is_per",
 "target" : "is_symm",
 "file" : "core/init/algebra/classes.lean",
 "line" : 112 }
 , { "name" : "name.lt.decidable_rel",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/meta/name.lean",
 "line" : 95 }
 , { "name" : "decidable_linear_order.to_linear_order",
 "topic" : "core",
 "source" : "decidable_linear_order",
 "target" : "linear_order",
 "file" : "core/init/algebra/order.lean",
 "line" : 215 }
 , { "name" : "is_linear_order.to_is_total",
 "topic" : "core",
 "source" : "is_linear_order",
 "target" : "is_total",
 "file" : "core/init/algebra/classes.lean",
 "line" : 108 }
 , { "name" : "prod.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 145 }
 , { "name" : "tactic.dsimp_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "native.float.has_div",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_div",
 "file" : "core/init/meta/float.lean",
 "line" : 69 }
 , { "name" : "smt_tactic.monad_state",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_state",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 66 }
 , { "name" : "add_left_cancel_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 106 }
 , { "name" : "char.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/data/char/basic.lean",
 "line" : 31 }
 , { "name" : "nat.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 17 }
 , { "name" : "has_zero.nonempty",
 "topic" : "logic",
 "source" : "has_zero",
 "target" : "nonempty",
 "file" : "logic/basic.lean",
 "line" : 882 }
 , { "name" : "name.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/name.lean",
 "line" : 81 }
 , { "name" : "char.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/char/basic.lean",
 "line" : 74 }
 , { "name" : "interactive.interactive.executor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "interactive.executor",
 "file" : "core/init/meta/tactic.lean",
 "line" : 120 }
 , { "name" : "native.rb_map.inhabited",
 "topic" : "meta",
 "source" : "decidable_rel",
 "target" : "inhabited",
 "file" : "meta/rb_map.lean",
 "line" : 79 }
 , { "name" : "except_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/except.lean",
 "line" : 52 }
 , { "name" : "expr.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 305 }
 , { "name" : "string.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/string/basic.lean",
 "line" : 32 }
 , { "name" : "monad_state_trans",
 "topic" : "core",
 "source" : "monad_state",
 "target" : "monad_state",
 "file" : "core/init/control/state.lean",
 "line" : 102 }
 , { "name" : "d_array.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/array/basic.lean",
 "line" : 132 }
 , { "name" : "expr.address.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 76 }
 , { "name" : "level.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/level.lean",
 "line" : 22 }
 , { "name" : "add_left_cancel_semigroup.to_add_semigroup",
 "topic" : "algebra",
 "source" : "add_left_cancel_semigroup",
 "target" : "add_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 106 }
 , { "name" : "set.has_union",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_union",
 "file" : "core/init/data/set.lean",
 "line" : 57 }
 , { "name" : "prod.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 68 }
 , { "name" : "list.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 53 }
 , { "name" : "monad_state.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/state.lean",
 "line" : 94 }
 , { "name" : "except_t.monad_run",
 "topic" : "core",
 "source" : "monad_run",
 "target" : "monad_run",
 "file" : "core/init/control/except.lean",
 "line" : 144 }
 , { "name" : "option.has_to_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 133 }
 , { "name" : "add_group.to_add_monoid",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "add_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 230 }
 , { "name" : "group.to_monoid",
 "topic" : "algebra",
 "source" : "group",
 "target" : "monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 226 }
 , { "name" : "binder_info.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/expr.lean",
 "line" : 48 }
 , { "name" : "options.has_add",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_add",
 "file" : "core/init/meta/options.lean",
 "line" : 25 }
 , { "name" : "coe_trans",
 "topic" : "core",
 "source" : "has_coe",
 "target" : "has_coe_t",
 "file" : "core/init/coe.lean",
 "line" : 95 }
 , { "name" : "list.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/data/list/instances.lean",
 "line" : 15 }
 , { "name" : "option.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/option/basic.lean",
 "line" : 69 }
 , { "name" : "smt_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "nat.has_div",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_div",
 "file" : "core/init/data/nat/div.lean",
 "line" : 18 }
 , { "name" : "expr.has_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/expr.lean",
 "line" : 275 }
 , { "name" : "monad_run.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/lift.lean",
 "line" : 80 }
 , { "name" : "int.has_mod",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mod",
 "file" : "core/init/data/int/basic.lean",
 "line" : 315 }
 , { "name" : "preorder.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/algebra/order.lean",
 "line" : 19 }
 , { "name" : "punit.subsingleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "core/init/data/punit.lean",
 "line" : 15 }
 , { "name" : "strict_weak_order.is_equiv",
 "topic" : "core",
 "source" : "is_strict_weak_order",
 "target" : "is_equiv",
 "file" : "core/init/algebra/classes.lean",
 "line" : 220 }
 , { "name" : "tactic.proof_state.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/core.lean",
 "line" : 1781 }
 , { "name" : "option.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 59 }
 , { "name" : "applicative.to_has_pure",
 "topic" : "core",
 "source" : "applicative",
 "target" : "has_pure",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "lift_fn_dom",
 "topic" : "core",
 "source" : "has_lift",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 176 }
 , { "name" : "comm_group.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 298 }
 , { "name" : "nat.has_one",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_one",
 "file" : "core/init/core.lean",
 "line" : 427 }
 , { "name" : "congr_arg_kind.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "expr.has_to_pexpr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_pexpr",
 "file" : "core/init/meta/pexpr.lean",
 "line" : 42 }
 , { "name" : "reader_t.monad_functor",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_functor",
 "file" : "core/init/control/reader.lean",
 "line" : 50 }
 , { "name" : "unification_constraint.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "bool.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 100 }
 , { "name" : "comm_monoid.to_monoid",
 "topic" : "algebra",
 "source" : "comm_monoid",
 "target" : "monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 203 }
 , { "name" : "tactic.binder_info.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/mk_dec_eq_instance.lean",
 "line" : 137 }
 , { "name" : "tactic_doc_entry.has_sizeof_inst",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "tactic/doc_commands.lean",
 "line" : 133 }
 , { "name" : "applicative.to_has_seq",
 "topic" : "core",
 "source" : "applicative",
 "target" : "has_seq",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "widget.filter_type.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/widget/interactive_expr.lean",
 "line" : 149 }
 , { "name" : "has_seq_left.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/applicative.lean",
 "line" : 21 }
 , { "name" : "tactic.andthen_seq_focus",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_andthen",
 "file" : "core/init/meta/tactic.lean",
 "line" : 1220 }
 , { "name" : "tagged_format.has_to_fmt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/tagged_format.lean",
 "line" : 49 }
 , { "name" : "coe_subtype",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/coe.lean",
 "line" : 161 }
 , { "name" : "native.float.has_neg",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_neg",
 "file" : "core/init/meta/float.lean",
 "line" : 65 }
 , { "name" : "lean.parser.reflectable.has_reflect",
 "topic" : "core",
 "source" : "lean.parser",
 "target" : "lean.parser.reflectable",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 141 }
 , { "name" : "state_t.has_monad_lift",
 "topic" : "core",
 "source" : "monad",
 "target" : "has_monad_lift",
 "file" : "core/init/control/state.lean",
 "line" : 59 }
 , { "name" : "list.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/data/list/basic.lean",
 "line" : 40 }
 , { "name" : "rbtree.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/data/rbtree/basic.lean",
 "line" : 169 }
 , { "name" : "widget.html.is_functor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "functor",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 279 }
 , { "name" : "has_well_founded_of_has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_well_founded",
 "file" : "core/init/wf.lean",
 "line" : 150 }
 , { "name" : "lift_base",
 "topic" : "core",
 "source" : "has_lift",
 "target" : "has_lift_t",
 "file" : "core/init/coe.lean",
 "line" : 92 }
 , { "name" : "applicative.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "lean.parser.has_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 133 }
 , { "name" : "smt_tactic.has_monad_lift",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_monad_lift",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 73 }
 , { "name" : "has_monad_lift.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/lift.lean",
 "line" : 21 }
 , { "name" : "subtype.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 71 }
 , { "name" : "option.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/data/option/basic.lean",
 "line" : 63 }
 , { "name" : "sum.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 62 }
 , { "name" : "native.float.has_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_le",
 "file" : "core/init/meta/float.lean",
 "line" : 132 }
 , { "name" : "pos.has_lt",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "tactic/core.lean",
 "line" : 16 }
 , { "name" : "unsigned.has_div",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_div",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 17 }
 , { "name" : "exceptional.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/exceptional.lean",
 "line" : 53 }
 , { "name" : "list.is_lawful_monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "core/init/data/list/instances.lean",
 "line" : 18 }
 , { "name" : "level.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/level.lean",
 "line" : 39 }
 , { "name" : "char.decidable_le",
 "topic" : "core",
 "source" : "char",
 "target" : "decidable",
 "file" : "core/init/data/char/basic.lean",
 "line" : 37 }
 , { "name" : "char.decidable_is_lower",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 42 }
 , { "name" : "binder.inhabited",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "meta/expr.lean",
 "line" : 181 }
 , { "name" : "tactic.delta_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 213 }
 , { "name" : "eq_is_equiv",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_equiv",
 "file" : "core/init/algebra/classes.lean",
 "line" : 127 }
 , { "name" : "dlist.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/data/dlist.lean",
 "line" : 60 }
 , { "name" : "unification_hint.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "congr_arg_kind.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/congr_lemma.lean",
 "line" : 22 }
 , { "name" : "psum.has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 505 }
 , { "name" : "semigroup.to_is_associative",
 "topic" : "algebra",
 "source" : "semigroup",
 "target" : "is_associative",
 "file" : "algebra/group/defs.lean",
 "line" : 69 }
 , { "name" : "lift_pair₂",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 185 }
 , { "name" : "fun_info.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 40 }
 , { "name" : "left_cancel_semigroup.to_semigroup",
 "topic" : "algebra",
 "source" : "left_cancel_semigroup",
 "target" : "semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 101 }
 , { "name" : "int.has_neg",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_neg",
 "file" : "core/init/data/int/basic.lean",
 "line" : 85 }
 , { "name" : "monoid.to_semigroup",
 "topic" : "algebra",
 "source" : "monoid",
 "target" : "semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 166 }
 , { "name" : "comm_semigroup.to_is_commutative",
 "topic" : "algebra",
 "source" : "comm_semigroup",
 "target" : "is_commutative",
 "file" : "algebra/group/defs.lean",
 "line" : 94 }
 , { "name" : "inhabited.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/logic.lean",
 "line" : 770 }
 , { "name" : "monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 166 }
 , { "name" : "prod.has_well_founded",
 "topic" : "core",
 "source" : "has_well_founded",
 "target" : "has_well_founded",
 "file" : "core/init/wf.lean",
 "line" : 200 }
 , { "name" : "coe_fn_trans",
 "topic" : "core",
 "source" : "has_coe_t_aux",
 "target" : "has_coe_to_fun",
 "file" : "core/init/coe.lean",
 "line" : 132 }
 , { "name" : "is_symm_op_of_is_commutative",
 "topic" : "core",
 "source" : "is_commutative",
 "target" : "is_symm_op",
 "file" : "core/init/algebra/classes.lean",
 "line" : 16 }
 , { "name" : "left_cancel_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 101 }
 , { "name" : "add_comm_group.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 301 }
 , { "name" : "widget.interactive_expression.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/widget/interactive_expr.lean",
 "line" : 36 }
 , { "name" : "name.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/name.lean",
 "line" : 78 }
 , { "name" : "cc_state.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/smt/congruence_closure.lean",
 "line" : 86 }
 , { "name" : "vm_core.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/vm.lean",
 "line" : 79 }
 , { "name" : "fin.has_mod",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_mod",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 60 }
 , { "name" : "list.has_le",
 "topic" : "core",
 "source" : "has_lt",
 "target" : "has_le",
 "file" : "core/init/data/list/basic.lean",
 "line" : 330 }
 , { "name" : "list.has_union",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "has_union",
 "file" : "core/init/data/list/basic.lean",
 "line" : 240 }
 , { "name" : "lean.parser.reflectable.cast",
 "topic" : "core",
 "source" : "lean.parser",
 "target" : "lean.parser.reflectable",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 138 }
 , { "name" : "congr_arg_kind.decidable_eq",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "meta/expr.lean",
 "line" : null }
 , { "name" : "bool.decidable_forall_bool",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "data/bool.lean",
 "line" : 79 }
 , { "name" : "pprod.inhabited",
 "topic" : "tactic",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "string.has_append",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "core/init/data/string/basic.lean",
 "line" : 149 }
 , { "name" : "binder.has_to_tactic_format",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "meta/expr.lean",
 "line" : 195 }
 , { "name" : "is_total_preorder.to_is_trans",
 "topic" : "core",
 "source" : "is_total_preorder",
 "target" : "is_trans",
 "file" : "core/init/algebra/classes.lean",
 "line" : 100 }
 , { "name" : "format.color.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/format.lean",
 "line" : 11 }
 , { "name" : "has_well_founded.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/wf.lean",
 "line" : 27 }
 , { "name" : "fun_info.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "has_monad_lift_t_refl",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_monad_lift_t",
 "file" : "core/init/control/lift.lean",
 "line" : 40 }
 , { "name" : "except_t.monad_except",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_except",
 "file" : "core/init/control/except.lean",
 "line" : 117 }
 , { "name" : "comm_semigroup.to_semigroup",
 "topic" : "algebra",
 "source" : "comm_semigroup",
 "target" : "semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 76 }
 , { "name" : "expr.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/meta/expr.lean",
 "line" : 293 }
 , { "name" : "sum.is_lawful_functor",
 "topic" : "control",
 "source" : "[anonymous]",
 "target" : "is_lawful_functor",
 "file" : "control/basic.lean",
 "line" : 182 }
 , { "name" : "state_t.monad_state",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_state",
 "file" : "core/init/control/state.lean",
 "line" : 105 }
 , { "name" : "binder.has_to_format",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "meta/expr.lean",
 "line" : 194 }
 , { "name" : "is_per.to_is_trans",
 "topic" : "core",
 "source" : "is_per",
 "target" : "is_trans",
 "file" : "core/init/algebra/classes.lean",
 "line" : 112 }
 , { "name" : "unsigned.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 112 }
 , { "name" : "subsingleton_info.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 75 }
 , { "name" : "decidable.true",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 603 }
 , { "name" : "string.has_decidable_lt",
 "topic" : "core",
 "source" : "string",
 "target" : "decidable",
 "file" : "core/init/data/string/basic.lean",
 "line" : 29 }
 , { "name" : "hinst_lemmas.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/smt/ematch.lean",
 "line" : 53 }
 , { "name" : "id.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/control/id.lean",
 "line" : 14 }
 , { "name" : "native.float.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/float.lean",
 "line" : 147 }
 , { "name" : "smt_tactic.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 64 }
 , { "name" : "reader_t.alternative",
 "topic" : "core",
 "source" : "alternative",
 "target" : "alternative",
 "file" : "core/init/control/reader.lean",
 "line" : 62 }
 , { "name" : "unit.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 47 }
 , { "name" : "monad_state_adapter.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/state.lean",
 "line" : 159 }
 , { "name" : "widget.html.list_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 289 }
 , { "name" : "monad_functor_t_refl",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_functor_t",
 "file" : "core/init/control/lift.lean",
 "line" : 65 }
 , { "name" : "is_lawful_monad.to_is_lawful_applicative",
 "topic" : "core",
 "source" : "is_lawful_monad",
 "target" : "is_lawful_applicative",
 "file" : "core/init/control/lawful.lean",
 "line" : 44 }
 , { "name" : "list.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/data/list/basic.lean",
 "line" : 47 }
 , { "name" : "tactic.ex_to_tac",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/tactic.lean",
 "line" : 294 }
 , { "name" : "alternative.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/alternative.lean",
 "line" : 15 }
 , { "name" : "iff.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 707 }
 , { "name" : "tactic.andthen_seq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_andthen",
 "file" : "core/init/meta/tactic.lean",
 "line" : 1217 }
 , { "name" : "prod.has_repr",
 "topic" : "core",
 "source" : "has_repr",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 65 }
 , { "name" : "tactic.interactive.case_tag.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/case_tag.lean",
 "line" : 124 }
 , { "name" : "has_monad_lift_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/lift.lean",
 "line" : 27 }
 , { "name" : "except_t.monad_functor",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_functor",
 "file" : "core/init/control/except.lean",
 "line" : 86 }
 , { "name" : "eq.decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/algebra/order.lean",
 "line" : 227 }
 , { "name" : "list.decidable_eq",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "decidable_eq",
 "file" : "core/init/data/list/basic.lean",
 "line" : 33 }
 , { "name" : "list.has_to_tactic_format",
 "topic" : "core",
 "source" : "has_to_tactic_format",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 313 }
 , { "name" : "list.has_lt",
 "topic" : "core",
 "source" : "has_lt",
 "target" : "has_lt",
 "file" : "core/init/data/list/basic.lean",
 "line" : 306 }
 , { "name" : "lean.parser.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/meta/lean/parser.lean",
 "line" : 113 }
 , { "name" : "native.float.has_mul",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mul",
 "file" : "core/init/meta/float.lean",
 "line" : 67 }
 , { "name" : "char.decidable_is_whitespace",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 36 }
 , { "name" : "widget.component.has_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 243 }
 , { "name" : "string.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 143 }
 , { "name" : "monad_functor_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/lift.lean",
 "line" : 56 }
 , { "name" : "fin.has_mul",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_mul",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 59 }
 , { "name" : "except_t.is_lawful_monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "core/init/control/lawful.lean",
 "line" : 157 }
 , { "name" : "tactic.dunfold_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "unsigned.has_add",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_add",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 13 }
 , { "name" : "nat.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 109 }
 , { "name" : "option.lift_or_get_is_right_id",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "is_right_id",
 "file" : "data/option/defs.lean",
 "line" : 99 }
 , { "name" : "state_t.monad_run",
 "topic" : "core",
 "source" : "monad_run",
 "target" : "monad_run",
 "file" : "core/init/control/state.lean",
 "line" : 174 }
 , { "name" : "default_has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 479 }
 , { "name" : "native.float.decidable_le",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/meta/float.lean",
 "line" : 133 }
 , { "name" : "add_left_cancel_monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 218 }
 , { "name" : "native.rb_set.inhabited",
 "topic" : "meta",
 "source" : "decidable_rel",
 "target" : "inhabited",
 "file" : "meta/rb_map.lean",
 "line" : 22 }
 , { "name" : "semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 52 }
 , { "name" : "prop.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/logic.lean",
 "line" : 778 }
 , { "name" : "string.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/data/string/basic.lean",
 "line" : 25 }
 , { "name" : "sum.has_sizeof",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 498 }
 , { "name" : "options.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/options.lean",
 "line" : 28 }
 , { "name" : "add_left_cancel_monoid.to_add_left_cancel_semigroup",
 "topic" : "algebra",
 "source" : "add_left_cancel_monoid",
 "target" : "add_left_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 218 }
 , { "name" : "bool.decidable_exists_bool",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "data/bool.lean",
 "line" : 83 }
 , { "name" : "tagged_format.is_functor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "functor",
 "file" : "core/init/meta/tagged_format.lean",
 "line" : 35 }
 , { "name" : "cc_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "native.float.has_float_pow",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_pow",
 "file" : "core/init/meta/float.lean",
 "line" : 80 }
 , { "name" : "except_t.monad",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad",
 "file" : "core/init/control/except.lean",
 "line" : 89 }
 , { "name" : "environment.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/environment.lean",
 "line" : 213 }
 , { "name" : "decidable.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 40 }
 , { "name" : "list.has_decidable_lt",
 "topic" : "core",
 "source" : "list",
 "target" : "decidable",
 "file" : "core/init/data/list/basic.lean",
 "line" : 309 }
 , { "name" : "is_total_preorder.to_is_total",
 "topic" : "core",
 "source" : "is_total_preorder",
 "target" : "is_total",
 "file" : "core/init/algebra/classes.lean",
 "line" : 100 }
 , { "name" : "string.iterator.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 72 }
 , { "name" : "widget.local_collection.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/widget/interactive_expr.lean",
 "line" : 188 }
 , { "name" : "expr.has_coe_to_fun",
 "topic" : "core",
 "source" : "bool",
 "target" : "has_coe_to_fun",
 "file" : "core/init/meta/expr.lean",
 "line" : 147 }
 , { "name" : "fin.decidable_eq",
 "topic" : "core",
 "source" : "nat",
 "target" : "decidable_eq",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 51 }
 , { "name" : "add_right_cancel_semigroup.to_add_semigroup",
 "topic" : "algebra",
 "source" : "add_right_cancel_semigroup",
 "target" : "add_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 139 }
 , { "name" : "coe_base",
 "topic" : "core",
 "source" : "has_coe",
 "target" : "has_coe_t",
 "file" : "core/init/coe.lean",
 "line" : 98 }
 , { "name" : "pexpr.has_to_pexpr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_pexpr",
 "file" : "core/init/meta/pexpr.lean",
 "line" : 39 }
 , { "name" : "widget.interactive_expression.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/widget/interactive_expr.lean",
 "line" : 38 }
 , { "name" : "punit.reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/has_reflect.lean",
 "line" : 54 }
 , { "name" : "set.has_inter",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_inter",
 "file" : "core/init/data/set.lean",
 "line" : 63 }
 , { "name" : "native.rb_lmap.inhabited",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "meta/rb_map.lean",
 "line" : 144 }
 , { "name" : "expr.coord.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 41 }
 , { "name" : "char.decidable_is_alpha",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 45 }
 , { "name" : "pi.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/logic.lean",
 "line" : 781 }
 , { "name" : "state_t.monad",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad",
 "file" : "core/init/control/state.lean",
 "line" : 34 }
 , { "name" : "unit.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 56 }
 , { "name" : "rbnode.color.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/rbtree/basic.lean",
 "line" : 19 }
 , { "name" : "comm_group.to_comm_monoid",
 "topic" : "algebra",
 "source" : "comm_group",
 "target" : "comm_monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 298 }
 , { "name" : "nat_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/format.lean",
 "line" : 79 }
 , { "name" : "doc_category.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "ulift.has_sizeof_inst",
 "topic" : "core",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "core/init/logic.lean",
 "line" : 981 }
 , { "name" : "bool.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 37 }
 , { "name" : "fin.decidable_le",
 "topic" : "core",
 "source" : "fin",
 "target" : "decidable",
 "file" : "core/init/data/fin/basic.lean",
 "line" : 27 }
 , { "name" : "widget_override.interactive_expression.has_to_format",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "tactic/interactive_expr.lean",
 "line" : 49 }
 , { "name" : "monad_fail.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/monad_fail.lean",
 "line" : 11 }
 , { "name" : "ematch_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "preorder.to_has_le",
 "topic" : "core",
 "source" : "preorder",
 "target" : "has_le",
 "file" : "core/init/algebra/order.lean",
 "line" : 19 }
 , { "name" : "interaction_monad.result_has_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/meta/interaction_monad.lean",
 "line" : 29 }
 , { "name" : "list.is_lawful_singleton",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "is_lawful_singleton",
 "file" : "core/init/data/list/basic.lean",
 "line" : 234 }
 , { "name" : "option.monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad",
 "file" : "core/init/data/option/basic.lean",
 "line" : 55 }
 , { "name" : "rbtree.inhabited",
 "topic" : "tactic",
 "source" : "auto_param",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : 75 }
 , { "name" : "set.has_insert",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_insert",
 "file" : "core/init/data/set.lean",
 "line" : 46 }
 , { "name" : "param_info.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "lift_fn_range",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 173 }
 , { "name" : "add_monoid.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 170 }
 , { "name" : "tactic.pformat.has_to_tactic_format",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "tactic/core.lean",
 "line" : 1856 }
 , { "name" : "tactic.alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/meta/tactic.lean",
 "line" : 69 }
 , { "name" : "native.float.of_nat_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/float.lean",
 "line" : 139 }
 , { "name" : "has_one.nonempty",
 "topic" : "logic",
 "source" : "has_one",
 "target" : "nonempty",
 "file" : "logic/basic.lean",
 "line" : 884 }
 , { "name" : "native.float.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/float.lean",
 "line" : 149 }
 , { "name" : "d_array.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/array/basic.lean",
 "line" : 11 }
 , { "name" : "level.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/level.lean",
 "line" : 18 }
 , { "name" : "fin.has_div",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_div",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 61 }
 , { "name" : "option_t.has_monad_lift",
 "topic" : "core",
 "source" : "monad",
 "target" : "has_monad_lift",
 "file" : "core/init/control/option.lean",
 "line" : 48 }
 , { "name" : "and.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 687 }
 , { "name" : "list.has_insert",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "has_insert",
 "file" : "core/init/data/list/basic.lean",
 "line" : 229 }
 , { "name" : "has_coe_t.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/coe.lean",
 "line" : 42 }
 , { "name" : "list.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/data/list/basic.lean",
 "line" : 12 }
 , { "name" : "expr.address.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/expr_address.lean",
 "line" : 78 }
 , { "name" : "set.is_lawful_functor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_functor",
 "file" : "core/init/data/set.lean",
 "line" : 89 }
 , { "name" : "plift.inhabited",
 "topic" : "tactic",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "int.decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/data/int/basic.lean",
 "line" : 15 }
 , { "name" : "simp_lemmas.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 99 }
 , { "name" : "unsigned.reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/has_reflect.lean",
 "line" : 37 }
 , { "name" : "congr_arg_kind.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/meta/congr_lemma.lean",
 "line" : 28 }
 , { "name" : "string_imp.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "option.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 62 }
 , { "name" : "monoid_to_is_right_id",
 "topic" : "algebra",
 "source" : "monoid",
 "target" : "is_right_id",
 "file" : "algebra/group/defs.lean",
 "line" : 192 }
 , { "name" : "native.float.has_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_lt",
 "file" : "core/init/meta/float.lean",
 "line" : 129 }
 , { "name" : "option.has_reflect",
 "topic" : "core",
 "source" : "reflected",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "empty.subsingleton",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "subsingleton",
 "file" : "logic/basic.lean",
 "line" : 36 }
 , { "name" : "smt_tactic.has_coe",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 76 }
 , { "name" : "array.has_mem",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_mem",
 "file" : "core/init/data/array/basic.lean",
 "line" : 226 }
 , { "name" : "monad_reader.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/control/reader.lean",
 "line" : 83 }
 , { "name" : "applicative.to_has_seq_left",
 "topic" : "core",
 "source" : "applicative",
 "target" : "has_seq_left",
 "file" : "core/init/control/applicative.lean",
 "line" : 31 }
 , { "name" : "interactive.loc.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/interactive_base.lean",
 "line" : 24 }
 , { "name" : "list.nodup_decidable",
 "topic" : "data",
 "source" : "list",
 "target" : "decidable",
 "file" : "data/list/defs.lean",
 "line" : 449 }
 , { "name" : "tactic.apply_cfg.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/tactic.lean",
 "line" : 534 }
 , { "name" : "ordering.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "sort.inhabited",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "logic/basic.lean",
 "line" : 40 }
 , { "name" : "has_to_format_to_has_to_tactic_format",
 "topic" : "core",
 "source" : "has_to_format",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 330 }
 , { "name" : "nat.has_sub",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sub",
 "file" : "core/init/data/nat/basic.lean",
 "line" : 38 }
 , { "name" : "doc_category.decidable_eq",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "tactic/doc_commands.lean",
 "line" : 119 }
 , { "name" : "decidable_eq_of_subsingleton",
 "topic" : "logic",
 "source" : "subsingleton",
 "target" : "decidable_eq",
 "file" : "logic/basic.lean",
 "line" : 46 }
 , { "name" : "monad_except_adapter_trans",
 "topic" : "core",
 "source" : "monad_except_adapter",
 "target" : "monad_except_adapter",
 "file" : "core/init/control/except.lean",
 "line" : 136 }
 , { "name" : "tactic.has_append",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_append",
 "file" : "tactic/core.lean",
 "line" : 1859 }
 , { "name" : "is_equiv.to_is_preorder",
 "topic" : "core",
 "source" : "is_equiv",
 "target" : "is_preorder",
 "file" : "core/init/algebra/classes.lean",
 "line" : 110 }
 , { "name" : "option_t.monad_except",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_except",
 "file" : "core/init/control/option.lean",
 "line" : 61 }
 , { "name" : "tactic.unfold_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "native.float.dec_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/float.lean",
 "line" : 134 }
 , { "name" : "option.lift_or_get_assoc",
 "topic" : "data",
 "source" : "is_associative",
 "target" : "is_associative",
 "file" : "data/option/defs.lean",
 "line" : 87 }
 , { "name" : "option_t.is_lawful_monad",
 "topic" : "core",
 "source" : "is_lawful_monad",
 "target" : "is_lawful_monad",
 "file" : "core/init/control/lawful.lean",
 "line" : 231 }
 , { "name" : "lift_list",
 "topic" : "core",
 "source" : "has_lift_t",
 "target" : "has_lift",
 "file" : "core/init/coe.lean",
 "line" : 188 }
 , { "name" : "coe_option",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe_t",
 "file" : "core/init/coe.lean",
 "line" : 115 }
 , { "name" : "forall_prop_decidable",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 728 }
 , { "name" : "tactic.unfold_proj_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 243 }
 , { "name" : "tactic.simp_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 262 }
 , { "name" : "cc_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/smt/congruence_closure.lean",
 "line" : 9 }
 , { "name" : "native.float.decidable_lt",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/meta/float.lean",
 "line" : 130 }
 , { "name" : "set.has_singleton",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_singleton",
 "file" : "core/init/data/set.lean",
 "line" : 49 }
 , { "name" : "pempty.has_sizeof_inst",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "logic/basic.lean",
 "line" : 101 }
 , { "name" : "coe_trans_aux",
 "topic" : "core",
 "source" : "has_coe",
 "target" : "has_coe_t_aux",
 "file" : "core/init/coe.lean",
 "line" : 126 }
 , { "name" : "nat.decidable_dvd",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_rel",
 "file" : "core/init/data/nat/lemmas.lean",
 "line" : 1226 }
 , { "name" : "native.float.has_sub",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sub",
 "file" : "core/init/meta/float.lean",
 "line" : 63 }
 , { "name" : "option_t.monad",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad",
 "file" : "core/init/control/option.lean",
 "line" : 27 }
 , { "name" : "add_comm_monoid.to_add_comm_semigroup",
 "topic" : "algebra",
 "source" : "add_comm_monoid",
 "target" : "add_comm_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 207 }
 , { "name" : "setoid.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/setoid.lean",
 "line" : 10 }
 , { "name" : "options.has_decidable_eq",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "core/init/meta/options.lean",
 "line" : 21 }
 , { "name" : "string.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 106 }
 , { "name" : "partial_order.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/algebra/order.lean",
 "line" : 26 }
 , { "name" : "local_context.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/local_context.lean",
 "line" : 53 }
 , { "name" : "int.decidable_linear_order",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_linear_order",
 "file" : "core/init/data/int/order.lean",
 "line" : 190 }
 , { "name" : "except_t.monad_except_adapter",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_except_adapter",
 "file" : "core/init/control/except.lean",
 "line" : 139 }
 , { "name" : "name.reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/has_reflect.lean",
 "line" : 45 }
 , { "name" : "reader_t.monad",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad",
 "file" : "core/init/control/reader.lean",
 "line" : 38 }
 , { "name" : "id.monad_run",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_run",
 "file" : "core/init/control/id.lean",
 "line" : 17 }
 , { "name" : "decidable.false",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 606 }
 , { "name" : "setoid_has_equiv",
 "topic" : "core",
 "source" : "setoid",
 "target" : "has_equiv",
 "file" : "core/init/data/setoid.lean",
 "line" : 13 }
 , { "name" : "tactic.simp_intros_config.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "widget_override.filter_type.decidable_eq",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "tactic/interactive_expr.lean",
 "line" : 176 }
 , { "name" : "state_t.is_lawful_monad",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "is_lawful_monad",
 "file" : "core/init/control/lawful.lean",
 "line" : 127 }
 , { "name" : "pos.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/expr.lean",
 "line" : 21 }
 , { "name" : "pos.has_reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/derive.lean",
 "line" : null }
 , { "name" : "reader_t.monad_run",
 "topic" : "core",
 "source" : "monad_run",
 "target" : "monad_run",
 "file" : "core/init/control/reader.lean",
 "line" : 121 }
 , { "name" : "tactic.has_to_tactic_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_tactic_format",
 "file" : "core/init/meta/match_tactic.lean",
 "line" : 133 }
 , { "name" : "fin.has_to_string",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 56 }
 , { "name" : "environment.implicit_infer_kind.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/environment.lean",
 "line" : 55 }
 , { "name" : "decidable_linear_order.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/algebra/order.lean",
 "line" : 215 }
 , { "name" : "congr_arg_kind.has_reflect",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "meta/expr.lean",
 "line" : null }
 , { "name" : "add_comm_semigroup.to_is_commutative",
 "topic" : "algebra",
 "source" : "add_comm_semigroup",
 "target" : "is_commutative",
 "file" : "algebra/group/defs.lean",
 "line" : 94 }
 , { "name" : "comm_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 76 }
 , { "name" : "is_strict_total_order.to_is_trichotomous",
 "topic" : "core",
 "source" : "is_strict_total_order",
 "target" : "is_trichotomous",
 "file" : "core/init/algebra/classes.lean",
 "line" : 124 }
 , { "name" : "ematch_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/smt/ematch.lean",
 "line" : 144 }
 , { "name" : "coe_bool_to_Prop",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_coe",
 "file" : "core/init/coe.lean",
 "line" : 147 }
 , { "name" : "format.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/format.lean",
 "line" : 64 }
 , { "name" : "nat.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 112 }
 , { "name" : "or.decidable",
 "topic" : "core",
 "source" : "decidable",
 "target" : "decidable",
 "file" : "core/init/logic.lean",
 "line" : 693 }
 , { "name" : "unsigned.has_sub",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sub",
 "file" : "core/init/data/unsigned/ops.lean",
 "line" : 14 }
 , { "name" : "psum.inhabited_left",
 "topic" : "logic",
 "source" : "inhabited",
 "target" : "inhabited",
 "file" : "logic/basic.lean",
 "line" : 43 }
 , { "name" : "list.decidable_pairwise",
 "topic" : "data",
 "source" : "list",
 "target" : "decidable",
 "file" : "data/list/defs.lean",
 "line" : 398 }
 , { "name" : "state_t.monad_functor",
 "topic" : "core",
 "source" : "monad",
 "target" : "monad_functor",
 "file" : "core/init/control/state.lean",
 "line" : 66 }
 , { "name" : "char.decidable_is_alphanum",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "decidable_pred",
 "file" : "core/init/data/char/classes.lean",
 "line" : 51 }
 , { "name" : "char.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/data/char/basic.lean",
 "line" : 21 }
 , { "name" : "smt_tactic.interactive.executor",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "interactive.executor",
 "file" : "core/init/meta/smt/interactive.lean",
 "line" : 33 }
 , { "name" : "pempty.decidable_eq",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "logic/basic.lean",
 "line" : 101 }
 , { "name" : "char.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 132 }
 , { "name" : "smt_pre_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/smt/smt_tactic.lean",
 "line" : 29 }
 , { "name" : "bool.decidable_linear_order",
 "topic" : "data",
 "source" : "[anonymous]",
 "target" : "decidable_linear_order",
 "file" : "data/bool.lean",
 "line" : 149 }
 , { "name" : "list.has_to_string",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_to_string",
 "file" : "core/init/data/to_string.lean",
 "line" : 44 }
 , { "name" : "module_info.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/module_info.lean",
 "line" : 49 }
 , { "name" : "rsimp.config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/smt/rsimp.lean",
 "line" : 116 }
 , { "name" : "unit.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/format.lean",
 "line" : 130 }
 , { "name" : "doc_category.has_reflect",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "tactic/doc_commands.lean",
 "line" : 119 }
 , { "name" : "is_total_preorder_is_preorder",
 "topic" : "core",
 "source" : "is_total_preorder",
 "target" : "is_preorder",
 "file" : "core/init/algebra/classes.lean",
 "line" : 102 }
 , { "name" : "psigma.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 517 }
 , { "name" : "string.iterator_imp.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "dlist.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/data/dlist.lean",
 "line" : 14 }
 , { "name" : "right_cancel_semigroup.to_semigroup",
 "topic" : "algebra",
 "source" : "right_cancel_semigroup",
 "target" : "semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 133 }
 , { "name" : "interaction_monad.monad_fail",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "monad_fail",
 "file" : "core/init/meta/interaction_monad.lean",
 "line" : 94 }
 , { "name" : "tactic.simp_intros_config.has_sizeof_inst",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/meta/simp_tactic.lean",
 "line" : 358 }
 , { "name" : "param_info.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/fun_info.lean",
 "line" : 37 }
 , { "name" : "list.has_inter",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "has_inter",
 "file" : "core/init/data/list/basic.lean",
 "line" : 246 }
 , { "name" : "option.decidable_forall_mem",
 "topic" : "data",
 "source" : "option",
 "target" : "decidable",
 "file" : "data/option/defs.lean",
 "line" : 39 }
 , { "name" : "native.float.has_nat_pow",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_pow",
 "file" : "core/init/meta/float.lean",
 "line" : 153 }
 , { "name" : "sort.inhabited'",
 "topic" : "logic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "logic/basic.lean",
 "line" : 41 }
 , { "name" : "fin.has_zero",
 "topic" : "core",
 "source" : "nat",
 "target" : "has_zero",
 "file" : "core/init/data/fin/ops.lean",
 "line" : 55 }
 , { "name" : "tactic_state.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/tactic.lean",
 "line" : 35 }
 , { "name" : "module_info.has_to_format",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_format",
 "file" : "core/init/meta/module_info.lean",
 "line" : 50 }
 , { "name" : "bool.has_sizeof",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "core/init/core.lean",
 "line" : 528 }
 , { "name" : "left_cancel_monoid.to_monoid",
 "topic" : "algebra",
 "source" : "left_cancel_monoid",
 "target" : "monoid",
 "file" : "algebra/group/defs.lean",
 "line" : 212 }
 , { "name" : "binder_info.decidable_eq",
 "topic" : "meta",
 "source" : "[anonymous]",
 "target" : "decidable_eq",
 "file" : "meta/expr.lean",
 "line" : null }
 , { "name" : "vm_obj_kind.inhabited",
 "topic" : "tactic",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "tactic/derive_inhabited.lean",
 "line" : null }
 , { "name" : "group.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "has_sizeof",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 226 }
 , { "name" : "nat.reflect",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_reflect",
 "file" : "core/init/meta/has_reflect.lean",
 "line" : 31 }
 , { "name" : "except_t.has_monad_lift",
 "topic" : "core",
 "source" : "monad",
 "target" : "has_monad_lift",
 "file" : "core/init/control/except.lean",
 "line" : 74 }
 , { "name" : "sigma.has_repr",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_repr",
 "file" : "core/init/data/repr.lean",
 "line" : 68 }
 , { "name" : "is_lawful_applicative.to_is_lawful_functor",
 "topic" : "core",
 "source" : "is_lawful_applicative",
 "target" : "is_lawful_functor",
 "file" : "core/init/control/lawful.lean",
 "line" : 26 }
 , { "name" : "int.decidable_le",
 "topic" : "core",
 "source" : "int",
 "target" : "decidable",
 "file" : "core/init/data/int/order.lean",
 "line" : 26 }
 , { "name" : "tactic.interactive.case_tag.has_to_string",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "has_to_string",
 "file" : "core/init/meta/case_tag.lean",
 "line" : 172 }
 , { "name" : "add_group.to_right_cancel_add_semigroup",
 "topic" : "algebra",
 "source" : "add_group",
 "target" : "add_right_cancel_semigroup",
 "file" : "algebra/group/defs.lean",
 "line" : 272 }
 , { "name" : "option.decidable_eq",
 "topic" : "core",
 "source" : "decidable_eq",
 "target" : "decidable_eq",
 "file" : "core/init/data/option/basic.lean",
 "line" : 72 }
 , { "name" : "occurrences.inhabited",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "inhabited",
 "file" : "core/init/meta/occurrences.lean",
 "line" : 33 }
 , { "name" : "tactic.unsafe.type_context.type_context_alternative",
 "topic" : "core",
 "source" : "[anonymous]",
 "target" : "alternative",
 "file" : "core/init/meta/type_context.lean",
 "line" : 96 }
 , { "name" : "widget.html.to_string_coe",
 "topic" : "core",
 "source" : "has_to_string",
 "target" : "has_coe",
 "file" : "core/init/meta/widget/basic.lean",
 "line" : 284 }
 , { "name" : "add_semigroup.has_sizeof_inst",
 "topic" : "algebra",
 "source" : "[anonymous]",
 "target" : "has_sizeof",
 "file" : "algebra/group/defs.lean",
 "line" : 55 }
 ]
 }