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

Follow

@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

· · Web · 1 · 0 · 1

@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.

@lthms je ferais sans doute ça quand j'aurais un pc sous la main

Et merci de bien vouloir répondre à mes futures questions :)))

@lthms @na Tout pareil 😊 C'est toujours sympa de répondre à la plupart des questions Coq ☺️

@jin @MartinShadok @na Perso, ma ressource de base a été le Coq’art. La collection de livre Software Foundations est souvent conseillé aujourd’hui.

Une fois les bases acquises, il faut lire le manuel et lire du code pour « découvrir » les douze mille constructions de Coq et choisir celles qui te conviennent le mieux (Coq est de ces systèmes où il existe plein de manière de faire la même chose et il n'existe aucun consensus pour désigner un sous-ensemble « largement conseillé »).

Sign in to participate in the conversation
Pipou Academy

FR : Ceci est une instance queer, qui vise à être aussi confortable et safe que possible. Nouvelleaux élèves bienvenu'es !