2025.11.16
https://gyazo.com/a786a4184dfd40f2fa14f68238d6c2d1
思った
https://gyazo.com/e483d450719e780d06f23b25e3a014b5
定理証明支援系という題なのに全員Leanで多様性なさすぎる
メモ
https://gyazo.com/688c05a93b62242dd0fef8b6bdd9777b
頼むぞ！
思った
https://gyazo.com/7c4869206fb4aeb7644b14adde7e98d6
ここまではね
$ \mathbf{IL}(\mathsf{R}) \dashv \mathbf{IL}(\mathsf{R, W}) = \mathbf{IL}(\mathsf{R^*})を忘れていた
思った
Leanのキャッシュ戦略を少し変えた．.lake全体ではなく.lake/buildだけキャッシュするようにした．おそらくうまくいくはず…