You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We currently just put the literate (LaTeX) Agda in the HTML output, which produces a bunch of garbage. It would be nice to have good-looking HTML output as well, but I don't know what a good approach for this would be without a bunch of duplication.
The text was updated successfully, but these errors were encountered:
We currently just put the literate (LaTeX) Agda in the HTML output, which produces a bunch of garbage. It would be nice to have good-looking HTML output as well, but I don't know what a good approach for this would be without a bunch of duplication.
The text was updated successfully, but these errors were encountered: