default values in structure (lean4)

Stream: new members

[Yakov Pechersky]

What's the right way to get default fallback values for a structure?

structure Node :=
  val : Nat
  name : String := ""

#print Node.mk -- constructor Node.mk : Nat → String → Node

It's not mentioned in TPIL4 either