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

Note Detail

Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:26:53)
ACL2で証明した定理をそのまま移植するなら普通のAgdaじゃなくてCubical Agdaのほうが良さそう
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:51:37)
等式に方向があるのはACL2のメリットだと前から思ってはいたんだよなあ

---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-08 01:25:09)
あー、hcomp のところまで来て自分が Cubical Agda に抱いていたメンタルモデルがかなり間違っていることに気づいた。これパスでつなげるイメージを抱いたから線路的な的なもの組む感じになるのかと思ったけど全然そうじゃなくて高次立方体を構成していくことで等式の連鎖を実現する感じなのか