syntax for dependently typed structures with default values

Stream: lean4

[Mark Wilhelm]

If I do something like this --

structure Something (i: Nat) where
  n1: Nat := 1
  n2: Nat := 1 + i

constant s : Something 10 := {}

...I see an error on s -- "(kernel) kernel type checker does not support meta variables". Is there a way to get this to work?

[Henrik Böving]

The elaborator does seem to at least partially understand what to do here since it ends up with:

[Elab.definition.body] foo : Something 10 :=
{ n1 := 1, n2 := ?m.938 + 1 }

so maybe that's something that Elab.struct just isn't doing yet? In this special case it at least seems feasible to me to infer the value for this meta variable

[Leonardo de Moura]

Pushed a fix for this issue https://github.com/leanprover/lean4/commit/66c82dadc96e021965d953f1b7a1edc372561005

[Mark Wilhelm]

Thank you for the fix