Created
July 9, 2020 18:10
-
-
Save jcommelin/46f68be10416f645241a0deb4da66327 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ "nodes" : | |
[{ "name" : "partial_order", | |
"topic" : "core", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 26 } | |
, { "name" : "has_ssubset", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 340 } | |
, { "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" : "comm_group", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 298 } | |
, { "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" : "has_seq_left", | |
"topic" : "core", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 21 } | |
, { "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_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" : "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" : "has_append", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 333 } | |
, { "name" : "subsingleton", | |
"topic" : "core", | |
"file" : "core/init/logic.lean", | |
"line" : 802 } | |
, { "name" : "has_add", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 323 } | |
, { "name" : "decidable_linear_order", | |
"topic" : "core", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 215 } | |
, { "name" : "has_neg", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 326 } | |
, { "name" : "add_right_cancel_semigroup", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 139 } | |
, { "name" : "add_group", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 230 } | |
, { "name" : "has_to_string", | |
"topic" : "core", | |
"file" : "core/init/data/to_string.lean", | |
"line" : 19 } | |
, { "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" : "applicative", | |
"topic" : "core", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "name" : "has_sizeof", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 464 } | |
, { "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" : "functor", | |
"topic" : "core", | |
"file" : "core/init/control/functor.lean", | |
"line" : 11 } | |
, { "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" : "monad", | |
"topic" : "core", | |
"file" : "core/init/control/monad.lean", | |
"line" : 23 } | |
, { "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_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" : "has_pure", | |
"topic" : "core", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 11 } | |
, { "name" : "right_cancel_semigroup", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 133 } | |
, { "name" : "has_inv", | |
"topic" : "core", | |
"file" : "core/init/core.lean", | |
"line" : 325 } | |
, { "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" : "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" : "add_monoid", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 170 } | |
, { "name" : "inhabited", | |
"topic" : "core", | |
"file" : "core/init/logic.lean", | |
"line" : 770 } | |
, { "name" : "has_orelse", | |
"topic" : "core", | |
"file" : "core/init/control/alternative.lean", | |
"line" : 10 } | |
, { "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" : "add_semigroup", | |
"topic" : "algebra", | |
"file" : "algebra/group/defs.lean", | |
"line" : 55 } | |
] | |
, | |
"edges" : | |
[{ "name" : "group.to_has_inv", | |
"topic" : "algebra", | |
"source" : "group", | |
"target" : "has_inv", | |
"file" : "algebra/group/defs.lean", | |
"line" : 226 } | |
, { "name" : "preorder.to_has_lt", | |
"topic" : "core", | |
"source" : "preorder", | |
"target" : "has_lt", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 19 } | |
, { "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" : "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" : "alternative.to_applicative", | |
"topic" : "core", | |
"source" : "alternative", | |
"target" : "applicative", | |
"file" : "core/init/control/alternative.lean", | |
"line" : 15 } | |
, { "name" : "group.to_left_cancel_semigroup", | |
"topic" : "algebra", | |
"source" : "group", | |
"target" : "left_cancel_semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 267 } | |
, { "name" : "monoid_to_is_left_id", | |
"topic" : "algebra", | |
"source" : "monoid", | |
"target" : "is_left_id", | |
"file" : "algebra/group/defs.lean", | |
"line" : 188 } | |
, { "name" : "add_monoid_to_is_right_id", | |
"topic" : "algebra", | |
"source" : "add_monoid", | |
"target" : "is_right_id", | |
"file" : "algebra/group/defs.lean", | |
"line" : 192 } | |
, { "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" : "add_group.to_has_neg", | |
"topic" : "algebra", | |
"source" : "add_group", | |
"target" : "has_neg", | |
"file" : "algebra/group/defs.lean", | |
"line" : 230 } | |
, { "name" : "comm_group.to_group", | |
"topic" : "algebra", | |
"source" : "comm_group", | |
"target" : "group", | |
"file" : "algebra/group/defs.lean", | |
"line" : 298 } | |
, { "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" : "add_monoid.to_add_semigroup", | |
"topic" : "algebra", | |
"source" : "add_monoid", | |
"target" : "add_semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 170 } | |
, { "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" : "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" : "monad.to_has_bind", | |
"topic" : "core", | |
"source" : "monad", | |
"target" : "has_bind", | |
"file" : "core/init/control/monad.lean", | |
"line" : 23 } | |
, { "name" : "comm_monoid.to_comm_semigroup", | |
"topic" : "algebra", | |
"source" : "comm_monoid", | |
"target" : "comm_semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 203 } | |
, { "name" : "add_comm_monoid.to_add_monoid", | |
"topic" : "algebra", | |
"source" : "add_comm_monoid", | |
"target" : "add_monoid", | |
"file" : "algebra/group/defs.lean", | |
"line" : 207 } | |
, { "name" : "add_comm_group.to_add_group", | |
"topic" : "algebra", | |
"source" : "add_comm_group", | |
"target" : "add_group", | |
"file" : "algebra/group/defs.lean", | |
"line" : 301 } | |
, { "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" : "add_monoid_to_is_left_id", | |
"topic" : "algebra", | |
"source" : "add_monoid", | |
"target" : "is_left_id", | |
"file" : "algebra/group/defs.lean", | |
"line" : 188 } | |
, { "name" : "add_semigroup.to_is_associative", | |
"topic" : "algebra", | |
"source" : "add_semigroup", | |
"target" : "is_associative", | |
"file" : "algebra/group/defs.lean", | |
"line" : 69 } | |
, { "name" : "add_comm_semigroup.to_add_semigroup", | |
"topic" : "algebra", | |
"source" : "add_comm_semigroup", | |
"target" : "add_semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 81 } | |
, { "name" : "add_group_has_sub", | |
"topic" : "algebra", | |
"source" : "add_group", | |
"target" : "has_sub", | |
"file" : "algebra/group/defs.lean", | |
"line" : 285 } | |
, { "name" : "semigroup.to_has_mul", | |
"topic" : "algebra", | |
"source" : "semigroup", | |
"target" : "has_mul", | |
"file" : "algebra/group/defs.lean", | |
"line" : 52 } | |
, { "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" : "alternative.to_has_orelse", | |
"topic" : "core", | |
"source" : "alternative", | |
"target" : "has_orelse", | |
"file" : "core/init/control/alternative.lean", | |
"line" : 15 } | |
, { "name" : "applicative.to_has_seq_right", | |
"topic" : "core", | |
"source" : "applicative", | |
"target" : "has_seq_right", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "name" : "monoid.to_has_one", | |
"topic" : "algebra", | |
"source" : "monoid", | |
"target" : "has_one", | |
"file" : "algebra/group/defs.lean", | |
"line" : 166 } | |
, { "name" : "add_semigroup.to_has_add", | |
"topic" : "algebra", | |
"source" : "add_semigroup", | |
"target" : "has_add", | |
"file" : "algebra/group/defs.lean", | |
"line" : 55 } | |
, { "name" : "decidable_eq_of_decidable_le", | |
"topic" : "core", | |
"source" : "decidable_rel", | |
"target" : "decidable_eq", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 203 } | |
, { "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" : "linear_order.to_partial_order", | |
"topic" : "core", | |
"source" : "linear_order", | |
"target" : "partial_order", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 30 } | |
, { "name" : "monad.to_applicative", | |
"topic" : "core", | |
"source" : "monad", | |
"target" : "applicative", | |
"file" : "core/init/control/monad.lean", | |
"line" : 23 } | |
, { "name" : "nonempty_of_inhabited", | |
"topic" : "core", | |
"source" : "inhabited", | |
"target" : "nonempty", | |
"file" : "core/init/logic.lean", | |
"line" : 794 } | |
, { "name" : "partial_order.to_preorder", | |
"topic" : "core", | |
"source" : "partial_order", | |
"target" : "preorder", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 26 } | |
, { "name" : "add_monoid.to_has_zero", | |
"topic" : "algebra", | |
"source" : "add_monoid", | |
"target" : "has_zero", | |
"file" : "algebra/group/defs.lean", | |
"line" : 170 } | |
, { "name" : "applicative.to_functor", | |
"topic" : "core", | |
"source" : "applicative", | |
"target" : "functor", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "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" : "has_zero.nonempty", | |
"topic" : "logic", | |
"source" : "has_zero", | |
"target" : "nonempty", | |
"file" : "logic/basic.lean", | |
"line" : 882 } | |
, { "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" : "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" : "applicative.to_has_pure", | |
"topic" : "core", | |
"source" : "applicative", | |
"target" : "has_pure", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "name" : "comm_monoid.to_monoid", | |
"topic" : "algebra", | |
"source" : "comm_monoid", | |
"target" : "monoid", | |
"file" : "algebra/group/defs.lean", | |
"line" : 203 } | |
, { "name" : "applicative.to_has_seq", | |
"topic" : "core", | |
"source" : "applicative", | |
"target" : "has_seq", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "name" : "has_well_founded_of_has_sizeof", | |
"topic" : "core", | |
"source" : "has_sizeof", | |
"target" : "has_well_founded", | |
"file" : "core/init/wf.lean", | |
"line" : 150 } | |
, { "name" : "semigroup.to_is_associative", | |
"topic" : "algebra", | |
"source" : "semigroup", | |
"target" : "is_associative", | |
"file" : "algebra/group/defs.lean", | |
"line" : 69 } | |
, { "name" : "left_cancel_semigroup.to_semigroup", | |
"topic" : "algebra", | |
"source" : "left_cancel_semigroup", | |
"target" : "semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 101 } | |
, { "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" : "comm_semigroup.to_semigroup", | |
"topic" : "algebra", | |
"source" : "comm_semigroup", | |
"target" : "semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 76 } | |
, { "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" : "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" : "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" : "comm_group.to_comm_monoid", | |
"topic" : "algebra", | |
"source" : "comm_group", | |
"target" : "comm_monoid", | |
"file" : "algebra/group/defs.lean", | |
"line" : 298 } | |
, { "name" : "preorder.to_has_le", | |
"topic" : "core", | |
"source" : "preorder", | |
"target" : "has_le", | |
"file" : "core/init/algebra/order.lean", | |
"line" : 19 } | |
, { "name" : "list.is_lawful_singleton", | |
"topic" : "core", | |
"source" : "decidable_eq", | |
"target" : "is_lawful_singleton", | |
"file" : "core/init/data/list/basic.lean", | |
"line" : 234 } | |
, { "name" : "has_one.nonempty", | |
"topic" : "logic", | |
"source" : "has_one", | |
"target" : "nonempty", | |
"file" : "logic/basic.lean", | |
"line" : 884 } | |
, { "name" : "option_t.has_monad_lift", | |
"topic" : "core", | |
"source" : "monad", | |
"target" : "has_monad_lift", | |
"file" : "core/init/control/option.lean", | |
"line" : 48 } | |
, { "name" : "list.has_insert", | |
"topic" : "core", | |
"source" : "decidable_eq", | |
"target" : "has_insert", | |
"file" : "core/init/data/list/basic.lean", | |
"line" : 229 } | |
, { "name" : "monoid_to_is_right_id", | |
"topic" : "algebra", | |
"source" : "monoid", | |
"target" : "is_right_id", | |
"file" : "algebra/group/defs.lean", | |
"line" : 192 } | |
, { "name" : "applicative.to_has_seq_left", | |
"topic" : "core", | |
"source" : "applicative", | |
"target" : "has_seq_left", | |
"file" : "core/init/control/applicative.lean", | |
"line" : 31 } | |
, { "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" : "decidable_eq_of_subsingleton", | |
"topic" : "logic", | |
"source" : "subsingleton", | |
"target" : "decidable_eq", | |
"file" : "logic/basic.lean", | |
"line" : 46 } | |
, { "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_equiv", | |
"topic" : "core", | |
"source" : "setoid", | |
"target" : "has_equiv", | |
"file" : "core/init/data/setoid.lean", | |
"line" : 13 } | |
, { "name" : "add_comm_semigroup.to_is_commutative", | |
"topic" : "algebra", | |
"source" : "add_comm_semigroup", | |
"target" : "is_commutative", | |
"file" : "algebra/group/defs.lean", | |
"line" : 94 } | |
, { "name" : "right_cancel_semigroup.to_semigroup", | |
"topic" : "algebra", | |
"source" : "right_cancel_semigroup", | |
"target" : "semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 133 } | |
, { "name" : "left_cancel_monoid.to_monoid", | |
"topic" : "algebra", | |
"source" : "left_cancel_monoid", | |
"target" : "monoid", | |
"file" : "algebra/group/defs.lean", | |
"line" : 212 } | |
, { "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" : "add_group.to_right_cancel_add_semigroup", | |
"topic" : "algebra", | |
"source" : "add_group", | |
"target" : "add_right_cancel_semigroup", | |
"file" : "algebra/group/defs.lean", | |
"line" : 272 } | |
] | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment