Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:14:58)
Cubical Agda で Vec の ++-assoc の定義についてどうすればわからなかったので標準ライブラリの答えをみてしまった。

Cubical Agda すごいな。PathP エレガントにインデックス側の +-assoc を処理できてる。これは、 Vec みたいな面倒くさい添え字尽きの依存型を活用するモチベーションがアップするのではないか
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:23:52)
こうなってくると結構 Cubical Agda 一択みたいな感じになり普通の Agda に戻る理由はないのでは。。。

---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:29:05)
一回 cong 縛りで List の定理を Cubical Agda で色々証明してみて Cubical Agda のパスの感覚を身体的になじませるか