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]
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]