Renaming abuse

Stream: general

[Yaël Dillies]

Consider this:

import order.conditionally_complete_lattice

set_option old_structure_cmd true

class conditionally_complete_linear_ordered_field (F : Type*)
  extends linear_ordered_field F, conditionally_complete_linear_order F

This fails with an exotic error:

invalid 'structure' header, field 'max_def' from 'conditionally_complete_linear_order' has already been declared with a different type
  auto_param (max = max_default)
    (name.mk_string "reflexivity" (name.mk_string "interactive" (name.mk_string "tactic" name.anonymous)))
and
  auto_param (sup = max_default)
    (name.mk_string "reflexivity" (name.mk_string "interactive" (name.mk_string "tactic" name.anonymous)))

and I believe the culprit is @Eric Wieser's #11309!

[Yaël Dillies]

In this specific case, I'm more than happy to not use old structures, but this seems to go against the style of the algebraic hierarchy.

[Eric Wieser]

We could always rename min to inf globally to make that specific problem go away, I just was too lazy too (as docs#linear_order is still in core)

[Yaël Dillies]

I believe it's in core because it's used to order actions within tactics.

[Yaël Dillies]

Solved it temporarily by renaming the fields myself.