Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Apparaît dans la collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques
Dans cet exposé je passerai en revue les surprises bonnes et moins bonnes je j'ai rencontrées en formalisant des mathématiques modernes en théorie des types dépendants.