D'après https://arxiv.org/abs/2003.01685, il semble qu'en Lean aussi, `Decidable` est défini comme une type classe. Ça vaudrait la peine de jeter un coup d'œil pour voir exactement comment ils l'utilisent.
Stefan
Afficher les réponses par date
Peut être que ça déjà été mentionné, mais c’est aussi le cas en Coq. Ça permet notamment d’avoir dans la librairie standard tous les lemmes en lien avec le tiers exclu.
Vincent
Le 20 janv. 2021 à 17:24, Stefan Monnier monnier@iro.umontreal.ca a écrit :
D'après https://arxiv.org/abs/2003.01685, il semble qu'en Lean aussi, `Decidable` est défini comme une type classe. Ça vaudrait la peine de jeter un coup d'œil pour voir exactement comment ils l'utilisent.
Stefan
Typer mailing list Typer@iro.umontreal.ca https://mailman.iro.umontreal.ca/cgi-bin/mailman/listinfo/typer