Zulip Chat Archive

Stream: general

Topic: opt_param vs default fields in structures

Eric Wieser (Jul 10 2022 at 10:38):

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 (Jul 10 2022 at 10:38):

Is this how opt_param is supposed to work?

Eric Wieser (Jul 10 2022 at 10:42):

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

Last updated: Aug 03 2023 at 10:10 UTC