search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
39 stars 7 forks source link

Σ型、依存和型を紹介する #431

Open Seasawher opened 3 months ago

Seasawher commented 3 months ago

TPiL: https://aconite-ac.github.io/theorem_proving_in_lean4_ja/dependent_type_theory.html#what-makes-dependent-type-theory-dependent-%E4%BD%95%E3%81%8C%E4%BE%9D%E5%AD%98%E5%9E%8B%E7%90%86%E8%AB%96%E3%82%92%E4%BE%9D%E5%AD%98%E3%81%9F%E3%82%89%E3%81%97%E3%82%81%E3%81%A6%E3%81%84%E3%82%8B%E3%81%AE%E3%81%8B

構造体になってる？