« Home

Tool. Use tr-agda to create literate agda card [tr-agda]

To create literate agda integration for tr-notes, I publish a new tool https://git.sr.ht/~dannypsnl/tr-agda, usage is

uv run tr-agda $(raco tr next ag)

You can provide title and taxon

uv run tr-agda $(raco tr next ag) --title [TITLE] --taxon [TAXON]