Proving Algebraic Datatypes are “Algebraic” in
soap.coffee/~lthms/posts/Algeb

It was fun to write, hope you enjoy reading it. I tried to spellcheck it, but tbh I wouldn’t be surprise to find mistakes… If you notice some, feel free to tell me!

@lthms "The associativity of sum is straightforward to prove, and should not pose a particular challenge to perspective readers; if we assume that this article is well-written, that is!" :)

I liked the article, seemed very well written and example good. I didn't understand everything, but that's probably because I'm just beginner in Coq and many of the tactics used I hadn't seen before.

I did bookmark it though. Maybe I can understand it later when I have better understanding of basics.

Sign in to participate in the conversation
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!