Topic: Renaming abuse
Yaël Dillies (Mar 08 2022 at 22:38):
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 (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