20 Jan
2021
20 Jan
'21
22:24
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