vscoqは3年前から更新されていないvscoqのバージョンを1.32くらいに下げると動くが、自動更新まわりの設定とか使い分けるのとかめんどいよく見ると↓に移動したらしいので入れてみたら動いたgithub.com Requirements node Installation git clone https://git…

TopProver で行われたCoqコンテストに参加して、モチベが上がったため、coqのライブラリを整備することに。 とりあえず便利なので累積帰納法を整備した。 自然数に関する累積帰納法だけだと不便なことがあるので、より一般化し、任意の型 X の f による nat …