型付き構造体の書き方、便利

Lean tips

({foo := "hello"} : Bar) の代わりに、{foo := "hello" : Bar} が使える。

namespace Temp
structure Bar where
  foo : String := "hello"
  baz : String := foo ++ "world"
#check {foo := "hi" : Bar}
#check { : Bar}
#eval  { : Bar}.baz

instance : ToString Bar where
 toString x := x.foo ++ " & " ++ x.baz
#eval toString { : Bar}
end Temp