Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
Apparaît dans la collection : Lean for the curious mathematician / Lean pour mathématiciens
In this talk, we introduce the Ssreflect tactic language, as used in the Mathematical Components library. We will focus on the tactics used to make formalization work lighter and easier to maintain.
