証明支援系に関することなら何でも
| SUN | MON | TUE | WED | THU | FRI | SAT |
|---|---|---|---|---|---|---|
1  Kitamado | 2 Kitamado | 3  SnO₂WMaN | 4 Kitamado | 5 | 6 | 7 |
8 | 9  Palalansoukî | 10 | 11 | 12 | 13 | 14  s-taiga |
15 SnO₂WMaN | 16 | 17 | 18 | 19  ネスけん。 | 20 | 21  wasabi315 |
22  梅崎直也 | 23 | 24 Kitamado | 25 |
- 12/1#lint コマンドの超軽い紹介
- 12/2Lean のマクロと Macro 型についてのかなり短い紹介
- 12/3スマリヤンのシステムについて
- 12/4#html コマンドの概要を雑に説明する
- 12/9強制法を用いてカット除去定理を証明する
- 12/14数学的帰納法を末尾再帰にする
- 12/15命題論理と様相論理のラベル付きシークエント計算をLeanで実装/証明する
- 12/19Lean4でバブルソートを書く
- 12/21パターンマッチの網羅性検査をAgdaで形式化する
- 12/22何か書きます
- 12/24Aesop タクティクで手軽に自動証明