fix: make header mapping type abbreviation (#546)

Make the type `HeaderMapping` an abbreviation instead of a definition.

This change was intended as part of
#539 and will make
leanprover/reference-manual#599 easier to
land. There's still [one place
remaining](https://github.com/leanprover/reference-manual/blob/main/Manual/Meta/ErrorExplanation.lean#L639-L640)
in `Manual/Meta/ErrorExplanation.lean` where it's relying on the
implementation of this type, which breaks if typeclass resolution
doesn't see the `ForIn` instance on `List`. Of course, we could also
expose `ForIn` on `HeaderMapping`, or expose a "close all sections for
this `HeaderMapping` but I'd rather decouple that decision from [the
present PR](leanprover/reference-manual#599).

Author: jcreedcmu

src/verso-manual/VersoManual/Markdown.lean

@@ -62,8 +62,7 @@ is understood as associating:
 We need to keep this state to appropriately repair non-consecutive
 Markdown header levels.
 -/
-public def HeaderMapping := List Nat
-deriving Inhabited
+public abbrev HeaderMapping := List Nat
 
 private structure MDState where
   inHeaders : HeaderMapping := []