SUMMARY.md

Functional Programming in Lean

Functional Programming in Lean イントロダクション Acknowledgments

• Lean を知る
  • 式の評価
  • 型
  • 関数と定義
  • 構造体
  • データ型・パターン・再帰
  • 多相性
  • その他の便利な機能
  • まとめ
• ハローワールド!
  • プログラムの実行
  • ステップ・バイ・ステップ
  • プロジェクトの開始
  • Worked Example: cat
  • Additional Conveniences
  • まとめ
• 休憩：命題・証明・リストの添え字アクセス
• オーバーロードと型クラス
  • 正の整数
  • 型クラスと多相性
  • インスタンス探索の制御
  • 配列と添え字アクセス
  • 標準クラス
  • 型強制
  • その他の便利な機能
  • まとめ
• モナド
  • モナド型クラス
  • 例：モナドにおける算術
  • モナドのための do 記法
  • IO モナド
  • その他の便利な機能
  • まとめ
• 関手・アプリカティブ関手・モナド
  • 構造体と継承
  • アプリカティブ関手
  • アプリカティブ関手の約定
  • オルタナティブ
  • 宇宙
  • 完全な定義
  • まとめ
• モナド変換子
  • IOとReaderを組み合わせる
  • モナド組み立てキット
  • モナド変換子の順序
  • さらなる do の機能
  • その他の便利な機能
  • まとめ
• 依存型によるプログラミング
  • 添字族
  • ユニバースによるデザインパターン
  • 使用事例：型付きクエリ
  • 添字・パラメータ・宇宙レベル
  • 依存型プログラミングの落とし穴
  • まとめ
• 休憩：タクティク・帰納法・証明
• プログラミング・証明・パフォーマンス
  • 末尾再帰
  • 同値の証明
  • 配列と関数の停止
  • その他の不等式
  • 安全な配列のインデックス
  • 挿入ソートと配列の更新
  • 特別な型
  • まとめ

次のステップ