Zulip Chat Archive

Stream: general

Topic: old_structure_cmd in structure literals


view this post on Zulip Mario Carneiro (Nov 05 2018 at 20:23):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 20:24):

this despite the fact that there are no structures being declared

view this post on Zulip Johannes Hölzl (Nov 05 2018 at 21:39):

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

view this post on Zulip Sebastian Ullrich (Nov 06 2018 at 08:10):

It does. Maybe it shouldn't.

view this post on Zulip Sebastian Ullrich (Nov 06 2018 at 08:11):

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.


Last updated: May 08 2021 at 09:11 UTC