« 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://repo.dannypsnl.me/tr-notes/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]