Automatic instance naming

Stream: general

[Yaël Dillies]

How do I know the name of an instance I haven't explicitly named? In my case, the instance is

import data.set.basic

class circular_preorder (α : Type*) extends has_btw α, has_sbtw α :=
(btw_refl (a : α) : btw a a a)
(btw_cyclic_left {a b c : α} : btw a b c → btw b c a)
(btw_trans_left {a b c d : α} : btw a b c → btw b d c → btw a d c)
(sbtw := λ a b c, btw a b c ∧ ¬btw c b a)
(sbtw_iff_btw_not_btw {a b c : α} : sbtw a b c ↔ (btw a b c ∧ ¬btw c b a) . order_laws_tac)

instance (α : Type*) [preorder α] : circular_preorder α :=
{ btw := λ a b c, (a ≤ b ∧ b ≤ c) ∨ (b ≤ c ∧ c ≤ a) ∨ (c ≤ a ∧ a ≤ b),
  sbtw := λ a b c, (a < b ∧ b < c) ∨ (b < c ∧ c < a) ∨ (c < a ∧ a < b),
  btw_refl := sorry,
  btw_cyclic_left := sorry,
  btw_trans_left := sorry,
  sbtw_iff_btw_not_btw := sorry }

[Eric Rodriguez]

you could just stick @[simps?] on it for an easy way

[Eric Rodriguez]

the instance naming code isn't too advanced though

[Eric Rodriguez]

so it should be pretty predictable

[Eric Wieser]

example (α : Type*) [preorder α] : circular_preorder α := by show_term { apply_instance } would also tell you

[Yaël Dillies]

Oh yeah it was really dumb. It tried to call it circular_order. Any way to change the heuristics?

[Eric Wieser]

I think this one is one you should expect to name by hand

[Eric Wieser]

preorder.to_circular_order would be a reasonable name.

[Eric Rodriguez]

if you wanna dig, the relevant code is here