I finished writing program of huffman encoding with ACL2 and proving that encoding and decoding well.

source code: git.tojo.tokyo/bookshelf.git/t

CI: ci.tojo.tokyo/jobs/bookshelf/4

tojo boosted
tojo boosted

Zara was worried about her digital freedom, but found a way out. Follow her *Escape to Freedom* in a new animated video from the Free Software Foundation (FSF). #UserFreedom #EscapetoFreedom u.fsf.org/escape-to-freedom

@bsmall2 One of my favorite hotkeys is 'Reply to post'. I use it just now.

I got result from this article. I should use (include-book "arithmetic-5/top" :dir :system) if use operator like `mod` or `floor`.


Show thread

Equivalance relation is very important for use ACL2. It expand rewrite rule. I'm finding interested equivalance relation examples.

What I think is that ACL2 is great prover for Lisp users.

I'm not bilingual now.But I studying English. I will be bilingual.

tojo boosted

#free #frei #libre #自由 #じゆう Are you bilingual and would you like to see the FSFs free software resources in more languages? Email campaigns@fsf.org and join the translations team. It's the most effective way to bring free software to the world.

I understand functional-instantion hints in ACL2.


The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!