This file is indexed.

/usr/share/lhs2tex-1.15/agda.fmt is in lhs2tex 1.15-4.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
%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

\RequirePackage[T1]{fontenc}
\RequirePackage[utf8x]{inputenc}
\RequirePackage{ucs}
\RequirePackage{amsfonts}

\providecommand\mathbbm{\mathbb}

% TODO: Define more of these ...
\DeclareUnicodeCharacter{737}{\textsuperscript{l}}
\DeclareUnicodeCharacter{8718}{\ensuremath{\blacksquare}}
\DeclareUnicodeCharacter{8759}{::}
\DeclareUnicodeCharacter{9669}{\ensuremath{\triangleleft}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
\DeclareUnicodeCharacter{10214}{\ensuremath{\llbracket}}
\DeclareUnicodeCharacter{10215}{\ensuremath{\rrbracket}}

% 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 "}"

% TODO: Make this configurable. IMHO, italics doesn't work well
% for Agda code.

\renewcommand\Varid[1]{\mathord{\textsf{#1}}}
\let\Conid\Varid
\newcommand\Keyword[1]{\textsf{\textbf{#1}}}
\EndFmtInput

%endif
%endif
%endif