No Such Blog or Diary
Home > Archives > 2021年01月28日
今日は朝から夜までずっと Coq と Ltac を相手に戦っていた．とりあえず，マジで目が疲れてるのか涙出る．
だがしかし，Ltac の動きがまだ把握しきれてない．特に Ltac の世界と Gallina の世界の切れ目がよく把握できてないので，変数名だと思ってるところを書き換えただけで想定通りに動いてくれなくなったりしてた．まだまだ修行が足りん．
そういえば Ltac2 は使いやすいのだろうか？ そのうち試してみよう．
Page Top