Luna-Flow/QED
このドキュメントは現在のブランチ状態を追跡します。
リポジトリの位置付け
kernel-first アーキテクチャと形式仕様、制御されたフロントエンドを持つ定理証明器プロジェクトです。
ドキュメント構成
README.mdにリポジトリ叙述とリリース基線を書く。doc_standard.mdに文書契約を書く。- モジュールまたはサブシステム配下に
api.md、tutorial.md、design.mdを置く。
モジュール概要
kernel: 主な実装はsrc/kernelにあります。parser: 主な実装はsrc/parserにあります。tactics: 主な実装はsrc/tacticsにあります。prover: 主な実装はsrc/proverにあります。spec: 主な実装はdoc/qed_formal_spec.typにあります。