agda-macros.tex

\newdimen\mathindent\mathindent\leftmargini
\usepackage[links,references]{latex/agda}
\usepackage{newunicodechar}
\newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}
\newunicodechar{←}{\ensuremath{\mathnormal\from}}
\newunicodechar{→}{\ensuremath{\mathnormal\to}}
\newunicodechar{↦}{\ensuremath{\mathnormal\mapsto}}
\newunicodechar{∀}{\ensuremath{\mathnormal\forall}}
\newunicodechar{≡}{\ensuremath{\mathrel{=}}}
\newunicodechar{β}{\ensuremath{\mathnormal\beta}}
\newunicodechar{Π}{\ensuremath{\mathnormal\Pi}}
\newunicodechar{ℕ}{\ensuremath{\mathnormal{\mathbb N}}}
\newunicodechar{ℤ}{\ensuremath{\mathnormal{\mathbb Z}}}
\newunicodechar{¹}{\ensuremath{\mathnormal{^1}}}
\newunicodechar{²}{\ensuremath{\mathnormal{^2}}}
\newunicodechar{∧}{\ensuremath{\mathnormal{\wedge}}}
\newunicodechar{∨}{\ensuremath{\mathnormal{̌\vee}}}