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

Note Detail

Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:12:33)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。

---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:21:28)
ACL2は、ぷよぷよの連鎖がどこで止まったか教えてくれて連鎖を始める前に戻して何度でも盤面を調整してやり直せるイメージ
Reply 
---Replies---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:26:53)
ACL2で証明した定理をそのまま移植するなら普通のAgdaじゃなくてCubical Agdaのほうが良さそう