of_bounded_lattice instances

Stream: general

[Yaël Dillies]

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]

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

[Eric Wieser]

Want to make a PR to do so?

[Yaël Dillies]

Sure!

[Yaël Dillies]

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

[Eric Wieser]

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

[Eric Wieser]

That link is at the bottom of the page