Json default arguments

Stream: lean4

[Leni Aniva]

Is there a way to make fromJson respect the default values of fields in a structure? e.g.

structure Struct1 where
  | n: Nat
  | name: String := ""
  deriving Lean.FromJson

which would not parse a dictionary of the form {"n": 0} since the name field is not supplied

[Eric Wieser]

So by "respect" you mean "ignore the fact they have defaults"?

[Eric Wieser]

This seems a bit of an odd thing to want; if you don't want {"n": 0} to be legal JSON, do you really still want {n := 0} to be legal Lean?

[Leni Aniva]

Eric Wieser said:

So by "respect" you mean "ignore the fact they have defaults"?

I want the parser to be able to parse {"n": 0} instead of giving an error

[Eric Wieser]

Oh, you mean it currently does not parse that input, not that you want it to reject that input!

[Eric Wieser]

I think this is probably just not implemented; we had this feature in Lean 3

[Leni Aniva]

I've submitted an issue for this one: https://github.com/leanprover/lean4/issues/2225