Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
Appears in 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.
