old_structure_cmd in structure literals

Stream: general

[Mario Carneiro]

Here's a strange discovery:

import order.complete_lattice

namespace lattice
set_option old_structure_cmd false

def complete_lattice.copy {α} (c : complete_lattice α)
  (le : α → α → Prop) (eq_le : le = @complete_lattice.le α c)
  (top : α) (eq_top : top = @complete_lattice.top α c)
  (bot : α) (eq_bot : bot = @complete_lattice.bot α c)
  (sup : α → α → α) (eq_sup : sup = @complete_lattice.sup α c)
  (inf : α → α → α) (eq_inf : inf = @complete_lattice.inf α c)
  (Sup : set α → α) (eq_Sup : Sup = @complete_lattice.Sup α c)
  (Inf : set α → α) (eq_Inf : Inf = @complete_lattice.Inf α c) :
  complete_lattice α :=
begin
  refine { le := le, top := top, bot := bot, sup := sup, inf := inf, Sup := Sup, Inf := Inf, ..};
    subst_vars,
  exact @complete_lattice.le_refl α c,
  exact @complete_lattice.le_trans α c,
  exact @complete_lattice.le_antisymm α c,
  exact @complete_lattice.le_sup_left α c,
  exact @complete_lattice.le_sup_right α c,
  exact @complete_lattice.sup_le α c,
  exact @complete_lattice.inf_le_left α c,
  exact @complete_lattice.inf_le_right α c,
  exact @complete_lattice.le_inf α c,
  exact @complete_lattice.le_top α c,
  exact @complete_lattice.bot_le α c,
  exact @complete_lattice.le_Sup α c,
  exact @complete_lattice.Sup_le α c,
  exact @complete_lattice.Inf_le α c,
  exact @complete_lattice.le_Inf α c
end
end lattice

If you put set_option old_structure_cmd true instead, this proof times out

[Mario Carneiro]

this despite the fact that there are no structures being declared

[Johannes Hölzl]

uff, luckily I didn't run into this. Does the { f := _, .. _} notation depend on old_structure_cmd?

[Sebastian Ullrich]

It does. Maybe it shouldn't.

[Sebastian Ullrich]

The structure instance notation is pretty complex and fragile in Lean 3. I'm really not sure what we should do with it in Lean 4.