[Agda] Literate Agda bit rot

[Nils Anders Danielsson]

On 2018-07-04 20:02, Philip Wadler wrote:
> The example of Literate Agda in the 2.4.0 CHANGELOG appears not to
> work. See below. Can someone please suggest a fix?

The changelog states that the example was tested using TeX Live 2012.
Perhaps it still works using an older version of TeX Live.

If you are willing to use LuaLaTeX or XeLaTeX, then the following code
seems to work:

   \documentclass{article}

   \usepackage{agda}
   % Support for sans-serif Greek. Note that loading this package might
   % lead to changes in the appearance of some non-Greek characters as
   % well.
   \usepackage[scale=0.9]{FiraSans}

   \begin{document}

   \begin{code}
   data αβγδεζθικλμνξρστυφχψω : Set₁ where

   postulate
     →⇒⇛⇉⇄↦⇨↠⇀⇁ : Set
   \end{code}

   \[
   ∀X [ ∅ ∉ X ⇒ ∃f:X ⟶  ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
   \]

   \end{document}

-- 
/NAD