SM
Shattered Memories
Home
Blog
CV
Aug 8, 2026
lean
结构体默认值
structure
Box
where
m
:=
0
def b
:
Box
:=
{}
#eval b -- { m := 0 } 默认值语法