Proving Algebraic Datatypes are “Algebraic” in #Coq
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.
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!