In https://beta.mathhub.info/library/document/aHR0cHM6Ly9pc2FiZWxsZS5pbi50dW0uZGUvQVZMLVRyZWVzL0FWTDIub21kb2M%3D?modules=https%3A%2F%2Fisabelle.in.tum.de%3FAVL-Trees.AVL2&declarations=https%3A%2F%2Fisabelle.in.tum.de%2F%3FAVL-Trees.AVL2%3FAVL2.raw_sum.tree%5C%3C%5Esub%3E0.sum.Sum_Type.map_raw_sum%7Cconst we see funnily rendered constant names. <img width="1087" alt="Screenshot 2021-03-26 at 15 07 04" src="https://user-images.githubusercontent.com/4037538/112644045-46fff800-8e45-11eb-93f9-6dc38af31f87.png">
In https://beta.mathhub.info/library/document/aHR0cHM6Ly9pc2FiZWxsZS5pbi50dW0uZGUvQVZMLVRyZWVzL0FWTDIub21kb2M%3D?modules=https%3A%2F%2Fisabelle.in.tum.de%3FAVL-Trees.AVL2&declarations=https%3A%2F%2Fisabelle.in.tum.de%2F%3FAVL-Trees.AVL2%3FAVL2.raw_sum.tree%5C%3C%5Esub%3E0.sum.Sum_Type.map_raw_sum%7Cconst

we see funnily rendered constant names.