Zulip Chat Archive

Stream: graph theory

Topic: naming conventions

Alena Gusakov (Jan 17 2021 at 23:49):

How do we feel about referring to the cardinality of the vertex fintype as card_verts? e.g.

lemma card_common_neighbors_lt_card_verts (v w : V) :
  fintype.card (G.common_neighbors v w) < fintype.card V

Alena Gusakov (Jan 17 2021 at 23:51):

We already have

lemma degree_lt_card_verts (G : simple_graph V) (v : V) : G.degree v < fintype.card V

but I think that might've been from another one of my PRs. Can totally change it if anyone doesn't like it

Bryan Gin-ge Chen (Jan 18 2021 at 06:06):

I think that's fine. It's worth documenting conventions like this in module docstrings.

Last updated: Aug 03 2023 at 10:10 UTC