agdaLatex documentation (#7283)

* Added headline for agdaLatex * Added a link to the git repository for agdaLatex
agda · May 17, 2024 · 8c0af66 · 8c0af66
1 parent 2d0fe9f
commit 8c0af66
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/doc/user-manual/tools/generating-latex.rst b/doc/user-manual/tools/generating-latex.rst
@@ -826,3 +826,8 @@ code.
 .. _hyperref: https://www.ctan.org/pkg/hyperref
 .. _catchfilebetweentags: https://www.ctan.org/pkg/catchfilebetweentags
 .. _ICU: http://site.icu-project.org/
+
+Generating lagda files directly from Agda using agdaLatex
+---------------------------------------------------------
+A tool for for creating lagda files and corresponding LaTeX files directly from Agda code has been created.
+See  <https://github.com/csetzer/agdaLatex>