when are struct field defaults evaluated?

Stream: lean4

[David Renshaw]

I'm trying to understand default values for struct fields.

-- a default field starting with `by` is apparently evaluated lazily:
structure Foo where
  x : Nat
  y : Nat
  h : x = y := by rfl
-- no error

def foo1 := Foo.mk 1 1
-- works

def foo2 := Foo.mk 1 2
-- as expected, an error:
-- tactic 'rfl' failed, equality lhs
--  1
-- is not definitionally equal to rhs
--  2

-- so far, so good

structure Bar where
  x : Nat
  y : Nat
  h : x = y := let () := (); by rfl
-- error:
-- tactic 'rfl' failed, equality lhs
--  x
-- is not definitionally equal to rhs
--  y


-- why is the `by rfl` eagerly evaluated for `Bar` but not `Foo`?
-- Is there some special casing around top-level `by`?

[David Renshaw]

I'm trying to read the code in https://github.com/leanprover/lean4/blob/b36b50adb2336cae9c7d9687eb9ebc679e82e427/src/Lean/Elab/Structure.lean to understand why the top-level by is treated differently, but it's slow going.

[Sebastian Ullrich]

Is there some special casing around top-level by?

Yes, exactly that. You can blame me for that, Lean 3 had an... also questionable separate syntax h : x = y . rfl for it.

[David Renshaw]

aha. And here is the parser for the special case: https://github.com/leanprover/lean4/blob/1f081ee6cb776b0dcf0de8aba0da04712d2867aa/src/Lean/Parser/Term.lean#L106