@lthms Justement, je pensais ne pas en avoir besoin. 😕
Mais bon, définir une mesure n'est pas très difficile, donc je vais l'utiliser ☺️

@MartinShadok Bon courage ! J’aime pas trop Program en règle générale, alors j’essaie de m’en tenir éloigné la plupart du temps. :D

@lthms Tout pareil ☺
Ou alors j’utilise le combinateur de point fixe de TLC. J’hésite ☺

@MartinShadok je connais pas ça tiens (c’est fou comme c’est dur d’avoir une vue d’ensemble de Coq...)

@MartinShadok TLC looks actually /very/ good. This is the #Haskeller in my talking I suppose, but “typeclass-based” looks like a very good idea to me.

@lthms If classical logic doesn't bother you, this definitely a good library 😊