Conversation

One thing I very strongly appreciate about Agda is how incredibly easy it is to generate HTML from proofs. Here's the generated HTML for the exercise I wrote yesterday, updated to account for some feedback: dependenttyp.es/classes/artifa

Brendan Zabarauskas

@brendanzab

Jan 2

It's so nice! When I like to click around the stdlib (agda.github.io/agda-stdlib/RE) sometimes when I am bored. Hoping that they publish cubical one day…

has a project like this for cubical

Replying to

and

Yeah I don't think it uses the agda HTML thingy - it's something custom

8:45 AM · Jan 2, 2022Twitter Web App

Replying to

and

More referring to this issue from

@OwoTizusa

that has been open for a few years: github.com/agda/cubical/i 😳

github.com

Add website generated with the HTML backend like the stdlib? · Issue #17 · agda/cubical

So we can browse this project easier. BTW I need an admin (like @UlfNorell) to enable gh-pages rendering for this repo.

Brendan Zabarauskas

@brendanzab

Jan 2

But yeah super thankful that

@plt_amy

's thing is around for learning stuff

Replying to

and

it's written in literate agda + markdown (.lagda.md) agda compiles that into .md files with HTML where the code blocks used to be then I run it through Pandoc with a frankly ungodly amount of filters to do everything else (KaTeX, diagrams, text links, table of contents, …)