You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
634 B
634 B
agda-reference-filter
A Pandoc filter for linking Agda identifiers in inline code blocks.
Usage
Compile your literate Agda file to Markdown (use --html-highlight=auto), then pandoc --filter agda-reference-filter -i output.md -o output.html to compile the Markdown to HTML. Inline code spans that are exactly the same as an identifier present in the raw HTML emitted by Agda (that is - either a definition or a reference) will be linked to the same place that Agda linked that identifier to.
agda --html-highlight=auto --html example.lagda.md
pandoc --filter agda-reference-filter -i example.md -o example.html