Proving Algebraic Datatypes are “Algebraic” in #Coq
https://soap.coffee/~lthms/posts/AlgebraicDatatypes.html
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 ooh, you finished it! I will reserve some time for reading it tomorrow. I don't think I can catch finer points this point of the evening anymore 😁
@tuturto feel free to share your thoughts and questions!
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!