opt_param vs default fields in structures

Stream: general

[Eric Wieser]

So it turns out that using opt_param is not the same as using (x : X := default) in a structure; defaults specified by opt_param are used in angle bracket syntax and by direct calls to mk, while defaults specified with := are used in {} syntax:

structure am_i_from_a_literal :=
(val : opt_param bool ff := tt)

#eval ({} : am_i_from_a_literal).val  -- tt
#eval (⟨⟩ : am_i_from_a_literal).val  -- ff
#eval am_i_from_a_literal.mk.val  -- ff

(set_option old_structure_cmd true makes no difference)

[Eric Wieser]

Is this how opt_param is supposed to work?

[Eric Wieser]

Can someone try this with Lean4's docs4#optParam?