j
k
j a
j l
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
Retour au fil de discussion
Retour à la liste