ACL2 で回文に関する定理を証明した。ACL2 で定理を書くのがうまくなってきている気がする。
https://git.tojo.tokyo/acl2-theorems.git/commit/palindrome-sandwich.lisp?id=658812d37e3be083623a63c9839ac056451df1cd
これを証明するのすごく大変だったんだけど後から見返すと全然大変じゃなさそうなの困る。
やっぱ、ACL2 は自動証明なので後からコードだけ読んでもそれがどうしたって感じになるなー。
大変だったアピールするためには解説記事書くしかないな
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!
大変だったアピールするためには解説記事書くしかないな