Default value in structure

Stream: lean4

[Markus Schmaus]

I'm trying to define a structure with a property which Lean can proof using decide. Here is a minimal example:

structure Two where
  x : Nat
  property : x = 2 := by decide

def a : Two := {x := 2}
def b := Two.mk 2
def c : Two := ⟨2⟩ -- fails

Both def a and def b work, but def c fails. How can I make def c work as well?

[Utensil Song]

def c : Two := ⟨2, rfl⟩ works, but I guess you want to omit it.

[Alex J. Best]

I'm not sure that's possible with Lean right now. the anonymous constructor syntax must have as many arguments as explicit arguments for the mk function, and apparently making autoParams implicit doesnt work

[Utensil Song]

I tried _, got don't know how to synthesize placeholder for argument 'property', then ..., got unexpected token '..'; expected term.

[James Gallicchio]

it does seem a bit .. of a footgun to use autoparams and also anonymous constructors.. seems like a recipe for unmaintainable code