rulec

ファイルの拡張子は .rule です。

rulec では、規則を、表と、そのまわりの計算、例外、ただし書きで書きます。rulec check は、宣言した範囲のすべての入力に答えがちょうど一つあることを証明し、単位とお金を確かめ、Lean の証明が検査し直す証明書を書きます。検査を通った規則だけが、12 の言語の普通の関数になります。

rulec には自分のサイトがあります：rulec のサイト。