Skip to content

itleigns/CoqHelper

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 
 
 
 
 

Repository files navigation

注意

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

CoqLint.c

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

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

algebra_tactic.v

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

About

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

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published