<div dir="ltr"><div>The example of Literate Agda in the 2.4.0 CHANGELOG appears not to work. See below. Can someone please suggest a fix?</div><div><br></div><div>By the way, the example in the change log is much more helpful than the one in the documentation at</div><div><br></div><div> <a href="https://agda.readthedocs.io/en/v2.5.4/tools/literate-programming.html?highlight=literate">https://agda.readthedocs.io/en/v2.5.4/tools/literate-programming.html?highlight=literate</a></div><div> <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda</a><br></div><div><br></div><div>May I suggest the latter two be updated? Cheers, -- P</div><div><br></div><div><br></div><div><div>bruichladdich$ more test.lagda </div><div>\documentclass{article}</div><div>\usepackage{agda}</div><div>\begin{document}</div><div><br></div><div>\begin{code}</div><div>data αβγδεζθικλμνξρστυφχψω : Set₁ where</div><div><br></div><div>postulate</div><div> →⇒⇛⇉⇄↦⇨↠⇀⇁ : Set</div><div>\end{code}</div><div><br></div><div>\[</div><div>∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]</div><div>\]</div><div>\end{document}</div><div>bruichladdich$ agda --latex test.lagda </div><div>bruichladdich$ cd latex/</div><div>bruichladdich$ pdflatex test</div><div>This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex)</div><div> restricted \write18 enabled.</div><div>entering extended mode</div><div>(./test.tex</div><div>LaTeX2e <2016/03/31></div><div>Babel <3.9r> and hyphenation patterns for 83 language(s) loaded.</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls</div><div>Document Class: article 2014/09/29 v1.4h Standard LaTeX document class</div><div>(/Users/wadler/Library/texmf/tex/latex/size10.clo)) (./agda.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg)</div><div>(/Users/wadler/Library/texmf/tex/latex/pdftex.def))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd))</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def)))) (./test.aux)</div><div>(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd)</div><div>(/Users/wadler/Library/texmf/tex/latex/supp-pdf.tex</div><div>[Loading MPS to PDF converter (version 2006.09.02).]</div><div>) (/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def</div><div>fontencoding T3 patched</div><div>) (/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-3.def)</div><div>! Undefined control sequence.</div><div>\u-default-945 #1->\textalpha </div><div> </div><div>l.20 \end{code}</div><div> </div><div>? </div></div><div><br></div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div>
</div>