lean


结构体默认值

structure Box where
  m := 0


def b : Box := {}
#eval b -- { m := 0 } 默认值语法