Proving Algebraic Datatypes are “Algebraic” in #Coqhttps://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 the parts I have read so far are super good and easy enough to follow. I made a mistake and tried reading it in the late evening though, so I couldn't make it to end.
But I'm definitely going read it through with thought. This is interesting stuff!
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!