testlib.h を使ったgenerator用のライブラリです。 vector<long long> select(n, m) から 要素をランダムに取り出します。戻り値はソートされています。 vector<long long> grouping(n, m, min_size=0) 個を グループにランダムに分けます。戻り値はグループサイズの配列です。計算</long></long>…

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