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

ソースコード： /- The State monad transformer. -/ prelude import Init.Control.Basic import Init.Control.Id import Init.Control.Except universe u v w def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) := σ → m (α × …