現在、おそらく最も強力な型システムを持つと思われるLean 4によるコード。型ファミリーや依存タプルを含む型を定義して、型チェックは型システムに任せる。プログラマは、データの整合性をチェックするようなコードは書かない。処理のみを書く。 /-- 既婚か…