Theorem Prover Leanの紹介 - Just $ A sandboxMicrosoftが開発したTheorem Prover Leanを紹介します. 特徴 他の言語と軽く比較する. あくまで個人的な感想です. Lean Coq*1 Agda Isabelle 証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic 開発環境 emacs emacs, CoqIDE emacs jEdit ドキュメント × ◎ ○ △ implicit parameter ○ ○ △ (型を使わないので不要) Equational Reasoning ○(builtinなものはOK. 独自演算子は条件付き) ？(知らない) ◎ ○(基本的にbuiltinなもののみサポート) 自動証明 ×(なし？) ○(auto, omegaなど) △(emacsのautoコマンド) ◎(auto,
