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 dans le premier exemple en rust la notation "List a" (dans le Box) est pas correcte
@na Ahah, mais tellement x). Ça m’apprendra à essayer d’écrire du rust sans compilateur. Merci !
@lthms de rien :)
Aussi, ici : "where unit models the nil case, and α + list α models the cons case." Ça devrait être un * non ?
(déso je rapporte les erreurs que je vois une à une mais je suis sûr portable et c'est plus pratique comme ça)
@na Indeed! C’est pratique pour moi aussi, je les corrige au fur et à mesure (:
@lthms j'ai tout lu et c'était très intéressant, je suis juste triste de pas avoir le niveau en Coq pour comprendre certaines démonstrations :(( merci d'avoir écrit ça en tout cas
@na Cool ! Si tu as des questions, hésite pas du coup. (:
@lthms je pense qu'il faudrait surtout que je prenne un tuto Coq et que je m'y mette sérieusement haha, sinon je vais te poser des questions pendant deux semaines je pense
@na La première étape un peu « facile » c’est sans doute d’installer Coq/CoqIDE et de regarder pas à pas comment se découpent les preuves.
Après dans cet article, pour les garder courtes, j’ai eu tendance à les réduire au maximum donc tu verras pas forcément grand chose x).
That being said, si un jour tu te mets à Coq, je répondrais à toutes les questions que tu pourras poser, pendant deux semaine ou plus \o/ avec plaisir.
