Skip to content

Instantly share code, notes, and snippets.

@jcommelin
Created July 9, 2020 18:10
Show Gist options
  • Save jcommelin/46f68be10416f645241a0deb4da66327 to your computer and use it in GitHub Desktop.
Save jcommelin/46f68be10416f645241a0deb4da66327 to your computer and use it in GitHub Desktop.
{ "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