agda.fmt

%if False
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% agda.fmt
%
% basic definitions for formatting agda code
%
% Permission is granted to include this file (or parts of this file) 
% literally into other documents, regardless of the conditions or 
% license applying to these documents.
%
% Andres Loeh, May 2009, ver 1.1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%endif
%if not lhs2tex_agda_fmt_read
%let lhs2tex_agda_fmt_read = True
%include polycode.fmt
%
%if style /= newcode
\ReadOnlyOnce{agda.fmt}%

%if lang == agda

\providecommand\mathbbm{\mathbb}

% TODO: This is in general not a good idea.
\providecommand\textepsilon{$\epsilon$}
\providecommand\textmu{$\mu$}

%subst keyword a = "\Keyword{" a "}"

%Actually, varsyms should not occur in Agda output.
%subst varsym a = "\Varid{" a "}"

\newcommand\Keyword[1]{\mathsf{\mathbf{#1}}}
\EndFmtInput

%endif
%endif
%endif