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
Something we discussed with @martinescardo a while ago. Making an issue here so that I don't forget about it.
Currently, all Agda files in TypeTopology have the .lagda extension. For reasons that I don't really understand, Agda can generate Markdown files only from files with extension .lagda.md. It is possible to generate HTML from .lagda files but this has the problem that the literate parts of the code are treated as code (i.e. are not wrapped in <p></p> tags) so it's not possible to make the formatting nice by adding a CSS file.
It seems that the best way to fix this is by converting .lagda files to .lagda.md files (in fact @martinescardo already wrote a script for this if I recall correctly). It would be great to make the HTML files generated from TypeTopology nicer by doing this and compiling through a Markdown processor.
The text was updated successfully, but these errors were encountered:
Something we discussed with @martinescardo a while ago. Making an issue here so that I don't forget about it.
Currently, all Agda files in
TypeTopology
have the.lagda
extension. For reasons that I don't really understand, Agda can generate Markdown files only from files with extension.lagda.md
. It is possible to generate HTML from.lagda
files but this has the problem that the literate parts of the code are treated as code (i.e. are not wrapped in<p></p>
tags) so it's not possible to make the formatting nice by adding a CSS file.It seems that the best way to fix this is by converting
.lagda
files to.lagda.md
files (in fact @martinescardo already wrote a script for this if I recall correctly). It would be great to make the HTML files generated fromTypeTopology
nicer by doing this and compiling through a Markdown processor.The text was updated successfully, but these errors were encountered: