構造体構文

tips Lean

':=' を使わなくなったようだ。structure/where 、マクロかも知れない。

structure WordCount where
  wordCount : Nat
  lineCount : Nat
  charCount : Nat
  inWord    : Bool

宣言文の並びなので、構造体もコンテキストの一種、特に指標の一種と考える。

インスタンスの書き方は、コンストラクタを使う

WordCount.mk 0 0 0 false

リテラル構文、ただし型アノテーションがないと型不明

{ 
  wordCount := 0,
  lineCount := 0,
  charCount := 0,
  inWord    := true 
}