2026-04-19 15:41 UTC
@jonmsterling But what's the solution?
Replies (1)
-
@MartinEscardo@mathstodon.xyz 2026-04-19 16:43
@andrejbauer asks "what's the solution?" To use as few packages as possible. I spent a long time, some months ago, trying to find a fix for cleverref. For my collaborator it worked, because they had an old version of LaTeX, but for me it didn't. It was so frustrating. I subscribe to @jonmsterling 's position of using Spartan LaTeX. In TypeTopology we use both Spartan MLTT, and even more Spartan Agda, deliberately.