Zulip Chat Archive

Stream: general

Topic: of_bounded_lattice instances


Yaël Dillies (Aug 02 2021 at 12:05):

Why are those not called bounded_lattice.to_semilattice_xxx_yyy?

@[priority 100] -- see Note [lower instance priority]
instance semilattice_inf_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
  semilattice_inf_top α :=
{ le_top := λ x, @le_top α _ x, ..bl }

@[priority 100] -- see Note [lower instance priority]
instance semilattice_inf_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
  semilattice_inf_bot α :=
{ bot_le := λ x, @bot_le α _ x, ..bl }

@[priority 100] -- see Note [lower instance priority]
instance semilattice_sup_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
  semilattice_sup_top α :=
{ le_top := λ x, @le_top α _ x, ..bl }

@[priority 100] -- see Note [lower instance priority]
instance semilattice_sup_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
  semilattice_sup_bot α :=
{ bot_le := λ x, @bot_le α _ x, ..bl }

Eric Wieser (Aug 02 2021 at 12:14):

Probably because we haven't documented that naming convention at #naming!

Eric Wieser (Aug 02 2021 at 12:14):

Want to make a PR to do so?

Yaël Dillies (Aug 02 2021 at 12:18):

Sure!

Yaël Dillies (Aug 02 2021 at 13:36):

Where is the relevant file? I'd have expected it to be docs.contribute.naming.

Eric Wieser (Aug 02 2021 at 13:51):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/contribute/naming.md

Eric Wieser (Aug 02 2021 at 13:51):

That link is at the bottom of the page


Last updated: Dec 20 2023 at 11:08 UTC