Zulip Chat Archive

Stream: general

Topic: Renaming abuse

Yaël Dillies (Mar 08 2022 at 22:38):

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)))
  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 (Mar 08 2022 at 22:41):

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 (Mar 08 2022 at 22:45):

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 (Mar 08 2022 at 22:45):

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

Yaël Dillies (Apr 01 2022 at 14:43):

Solved it temporarily by renaming the fields myself.

Last updated: Aug 03 2023 at 10:10 UTC