【Lean4】where

where

「この型の構造を、以下のフィールドを指定して作ります」という意味

Plaintext

def 名前 : 構造の型 where
  フィールド1 := 値1
  フィールド2 := 値2
  ...

def 名前 : 構造の型 where
  フィールド1 := 値1
  フィールド2 := 値2
  ...