itleigns/CoqHelper

Coqを使うときに役に立つツール

注意

このリポジトリのソースコードは個人用に作られています。自分が普段使うコマンドのみを考慮しています。

CoqLint.c

Coqのソースコードを受け取って整形されたソースコードを返す。以下のような整形をする。

• 無駄なスペースや改行を消す
• match A with Bのような場合分けで適切に改行しインデントを追加する

algebra_tactic.v

可換モノイド、可換群、環、可換環を表すRecordを定義しそれの恒等式を証明をするTacticを作りました。Tacticは使うと中で使うTacticを標準出力に出力します。使った後は消してその出力で置き換えることを想定しています。体も作っていますがTacticの中身は可換環のと同じで可換環としてみた恒等式にしか対応していません。