Which operator a printer kind stands for

Lean module Esm.Document.Math.Kinds, formal/Esm/Document/Math/Kinds.lean at 184aa13d35e5
Imports Esm.Document.Math.RoundTrip

theorem kindOf_table proved source

theorem kindOf_table {o : String} {k : OpK} (h : kindOf o = k)
    (hk : ∀ k', k ≠ .cmp k') (hu : ∀ k', k ≠ .un k') (hc : k ≠ .call) (hother : k ≠ .other) :
    (o, k) ∈ kindTable

A kind from the table names the operator the table gives it.

This module also proves 18 lemmas without doc comments; they are in the source.