Use Literate Agda? - Githubissues

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.

https://jonsterling.github.io/agda-calf/

Apache License 2.0

55 stars 2 forks source link

Use Literate Agda? #39

Open HarrisonGrodin opened 1 year ago

HarrisonGrodin commented 1 year ago

So far, we have .agda files. However, it might be worth using Literate Agda files .lagda.md, which lets us:

include prose describing our constructions, in Markdown (allowing for bold, math, links, etc.)
default-hide boring details

jonsterling commented 1 year ago

this sounds like a pretty good idea!

HarrisonGrodin commented 1 year ago

I've been thinking about it more, and it seems almost obvious in retrospect! Especially as we formalize more, using Literate Agda will mean we'll not only end up with formalizations of algorithms, but a readable (hopefully!) textbook with inline code snippets.