agda/notes/papers/iird/lhs2TeX.fmt

%subst verb a		= "\text{\tt " a "}"
%subst verbatim a	= "\begin{tabbing}\tt'n" a "'n\end{tabbing}'n"
%subst verbnl		= "\\'n\tt "
%if style == tt
%subst inline a  = "\text{\texfamily " a "}"
%subst thinspace = "\Sp "
%subst code a    = "\begin{tabbing}\texfamily'n" a "'n\end{tabbing}'n"
%subst comment a = "{\rmfamily-{}- " a "}"
%subst nested a  = "{\rmfamily\enskip\{- " a " -\}\enskip}"
%subst pragma a  = "{\rmfamily\enskip\{-\#" a " \#-\}\enskip}"
%subst spaces a  = a
%subst special a = a
%subst space     = "~"
%subst newline   = "\\'n\texfamily "
%subst conid a   = "{\itshape " a "}"
%subst varid a   = a
%subst consym a  = a
%subst varsym a  = a
%subst numeral a = a
%subst char a    = "''" a "''"
%subst string a  = "\char34 " a "\char34 "
%if underlineKeywords
%subst keyword a = "\uline{" a "}"
%else
%subst keyword a = "{\bfseries " a "}"
%endif
%format \         = "\char''10"
%format .         = "\char''00"
%if not spacePreserving
%format alpha     = "\char''02"
%format beta      = "\char''03"
%format gamma     = "\char''11"
%format delta     = "\char''12"
%format pi        = "\char''07"
%format infty     = "\char''16"
%format intersect = "\char''22"
%format union     = "\char''23"
%format forall    = "\char''24"
%format exists    = "\char''25"
%format not       = "\char''05"
%format &&        = "\char''04"
%format ||        = "\char''37"
%format <-        = "\char''06"
%format ->        = "\char''31"
%format ==        = "\char''36"
%format /=        = "\char''32"
%format <=        = "\char''34"
%format >=        = "\char''35"
%endif
%if meta
%format M.a = "\ensuremath{a}"
%format M.b = "\ensuremath{b}"
%format M.c = "\ensuremath{c}"
%format M.d = "\ensuremath{d}"
%format M.e = "\ensuremath{e}"
%format M.f = "\ensuremath{f}"
%format M.g = "\ensuremath{g}"
%format M.h = "\ensuremath{h}"
%format M.i = "\ensuremath{i}"
%format M.j = "\ensuremath{j}"
%format M.k = "\ensuremath{k}"
%format M.l = "\ensuremath{l}"
%format M.m = "\ensuremath{m}"
%format M.n = "\ensuremath{n}"
%format M.o = "\ensuremath{o}"
%format M.p = "\ensuremath{p}"
%format M.q = "\ensuremath{q}"
%format M.r = "\ensuremath{r}"
%format M.s = "\ensuremath{s}"
%format M.t = "\ensuremath{t}"
%format M.u = "\ensuremath{u}"
%format M.v = "\ensuremath{v}"
%format M.w = "\ensuremath{w}"
%format M.x = "\ensuremath{x}"
%format M.y = "\ensuremath{y}"
%format M.z = "\ensuremath{z}"
%format M.A = "\ensuremath{A}"
%format M.B = "\ensuremath{B}"
%format M.C = "\ensuremath{C}"
%format M.D = "\ensuremath{D}"
%format M.E = "\ensuremath{E}"
%format M.F = "\ensuremath{F}"
%format M.G = "\ensuremath{G}"
%format M.H = "\ensuremath{H}"
%format M.I = "\ensuremath{I}"
%format M.J = "\ensuremath{J}"
%format M.K = "\ensuremath{K}"
%format M.L = "\ensuremath{L}"
%format M.M = "\ensuremath{M}"
%format M.N = "\ensuremath{N}"
%format M.O = "\ensuremath{O}"
%format M.P = "\ensuremath{P}"
%format M.Q = "\ensuremath{Q}"
%format M.R = "\ensuremath{R}"
%format M.S = "\ensuremath{S}"
%format M.T = "\ensuremath{T}"
%format M.U = "\ensuremath{U}"
%format M.V = "\ensuremath{V}"
%format M.W = "\ensuremath{W}"
%format M.X = "\ensuremath{X}"
%format M.Y = "\ensuremath{Y}"
%format M.Z = "\ensuremath{Z}"
%format M.alpha   = "\ensuremath{\alpha}"
%format M.beta    = "\ensuremath{\beta}"
%format M.gamma   = "\ensuremath{\gamma}"
%format M.delta   = "\ensuremath{\delta}"
%format M.epsilon = "\ensuremath{\epsilon}"
%format M.zeta    = "\ensuremath{\zeta}"
%format M.eta     = "\ensuremath{\eta}"
%format M.theta   = "\ensuremath{\theta}"
%format M.iota    = "\ensuremath{\iota}"
%format M.kappa   = "\ensuremath{\kappa}"
%format M.lambda  = "\ensuremath{\lambda}"
%format M.mu      = "\ensuremath{\mu}"
%format M.nu      = "\ensuremath{\nu}"
%format M.xi      = "\ensuremath{\xi}"
%format M.pi      = "\ensuremath{\pi}"
%format M.rho     = "\ensuremath{\rho}"
%format M.sigma   = "\ensuremath{\sigma}"
%format M.tau     = "\ensuremath{\tau}"
%format M.upsilon = "\ensuremath{\upsilon}"
%format M.phi     = "\ensuremath{\phi}"
%format M.chi     = "\ensuremath{\chi}"
%format M.psi     = "\ensuremath{\psi}"
%format M.omega   = "\ensuremath{\omega}"
%format M.Gamma   = "\ensuremath{\Gamma}"
%format M.Delta   = "\ensuremath{\Delta}"
%format M.Theta   = "\ensuremath{\Theta}"
%format M.Lambda  = "\ensuremath{\Lambda}"
%format M.Xi      = "\ensuremath{\Xi}"
%format M.Pi      = "\ensuremath{\Pi}"
%format M.Sigma   = "\ensuremath{\Sigma}"
%format M.Upsilon = "\ensuremath{\Upsilon}"
%format M.Phi     = "\ensuremath{\Phi}"
%format M.Psi     = "\ensuremath{\Psi}"
%format M.Omega   = "\ensuremath{\Omega}"
%format M.forall  = "\ensuremath{\forall}"
%format M.exists  = "\ensuremath{\exists}"
%format M.not     = "\ensuremath{\neg}"
%format ==>       = "\ensuremath{\Longrightarrow}"
%format <==       = "\ensuremath{\Longleftarrow}"
%format /\        = "\ensuremath{\wedge}"
%format \/        = "\ensuremath{\vee}"
%format M.=       = "\ensuremath{=}"
%format M./=      = "\ensuremath{\neq}"
%format M.<       = "\ensuremath{<}"
%format M.<=      = "\ensuremath{\leq}"
%format M.>=      = "\ensuremath{\geq}"
%format M.>       = "\ensuremath{>}"
%endif
%elif style == newcode
%subst comment a        = "-- " a
%subst nested a         = "{- " a " -}"
%subst code a           = a "'n"
%subst newline          = "'n"
%subst dummy            =
%subst pragma a         = "{-# " a " #-}"
%subst numeral a        = a
%subst keyword a        = a
%subst spaces a         = a
%subst special a        = a
%subst space            = " "
%subst conid a          = a
%subst varid a          = a
%subst consym a         = a
%subst varsym a         = a
%subst char a           = "''" a "''"
%subst string a         = "'d" a "'d"
%elif style == math
%subst phantom a	= "\phantom{" a "\mbox{}}"
%subst comment a	= "\mbox{\qquad-{}- " a "}"
%subst nested a	        = "\mbox{\enskip\{- " a " -\}\enskip}"
%if array
%subst code a    	= "\[\begin{array}{@{}lcl}'n\hspace{\lwidth}&\hspace{\cwidth}&\\[-10pt]'n" a "'n\end{array}\]"
%subst column3 l c r	= "{}" l " & " c " & {" r "}"
%subst column1 a	= "\multicolumn{3}{@{}l}{" a "}"
%else
%subst code a    	= "\begin{tabbing}'n\qquad\=\hspace{\lwidth}\=\hspace{\cwidth}\=\+\kill'n" a "'n\end{tabbing}"
%subst column3 l c r	= "$" l "$ \> \makebox[\cwidth]{$" c "$} \> ${" r "}$"
%subst column1 a	= "${" a "}$"
%endif
%subst newline   	= "\\'n"
%subst blankline 	= "\\[1mm]'n"
%let anyMath            = True
%elif style == poly
%subst comment a	= "\mbox{\onelinecomment " a "}"
%subst nested a	        = "\mbox{\commentbegin " a " \commentend}"
%if array
%subst code a    	= "\['n\begin{parray}\SaveRestoreHook'n" a "\ColumnHook'n\end{parray}'n\]\resethooks'n"
%else
%subst code a    	= "\begingroup\par\noindent\advance\leftskip\mathindent\('n\begin{pboxed}\SaveRestoreHook'n" a "\ColumnHook'n\end{pboxed}'n\)\par\noindent\endgroup\resethooks'n"
%endif
%subst column c a       = "\column{" c "}{" a "}'n"
%subst fromto b e t     = "\fromto{" b "}{" e "}{{}" t "{}}'n"
%subst left             = "@{}l@{}"
%subst centered         = "@{}c@{}"
%subst dummycol         = "@{}l@{}"
%subst newline   	= "\nextline'n"
%subst blankline        = "\nextline[\blanklineskip]'n"
%subst indent n         = "\hsindent{" n "}"
%let anyMath            = True
%endif
%if anyMath
%let autoSpacing	= True
%subst dummy		= "\cdot "
%subst inline a  	= "\ensuremath{" a "}"
%subst hskip a	        = "\hskip" a "em\relax"
%subst pragma a         = "\mbox{\enskip\{-\#" a " \#-\}\enskip}"
%if latex209
%subst numeral a 	= "{\mathrm " a "}"
%subst keyword a 	= "{\mathbf " a "}"
%else
%subst numeral a 	= "\mathrm{" a "}"
%subst keyword a 	= "\mathbf{" a "}"
%endif
%subst spaces a		= a
%subst special a	= a
%subst space     	= "\;"
%subst conid a   	= "\Conid{" a "}"
%subst varid a   	= "\Varid{" a "}"
%subst consym a  	= "\mathbin{" a "}"
%subst varsym a  	= "\mathbin{" a "}"
%subst char a    	= "\text{\tt ''" a "''}"
%subst string a  	= "\text{\tt \char34 " a "\char34}"
%format _          = "\anonymous "
%format ->         = "\to "
%format <-         = "\leftarrow "
%format =>         = "\Rightarrow "
%format \          = "\lambda "
%format |          = "\mid "
%format {          = "\{\mskip1.5mu "
%format }          = "\mskip1.5mu\}"
%format [          = "[\mskip1.5mu "
%format ]          = "\mskip1.5mu]"
%format =          = "\mathrel{=}"
%format ..         = "\mathinner{\ldotp\ldotp}"
%format ~          =  "\mathord{\sim}"
%format @          =  "\mathord{@}"
%format .          = "\mathbin{\circ}"
%format !!         = "\mathbin{!!}"
%format ^          = "\mathbin{\uparrow}"
%format ^^         = "\mathbin{\uparrow\uparrow}"
%format **         = "\mathbin{**}"
%format /          = "\mathbin{/}"
%format `quot`     = "\mathbin{\Varid{`quot`}}"
%format `rem`      = "\mathbin{\Varid{`rem`}}"
%format `div`      = "\mathbin{\Varid{`div`}}"
%format `mod`      = "\mathbin{\Varid{`mod`}}"
%format :%         = "\mathbin{:\%}"
%format %          = "\mathbin{\%}"
%format :          = "\mathbin{:}"
%format ++         = "\plus "
%format ==         = "\equiv "
%% ODER: format ==         = "\mathrel{==}"
%format /=         = "\not\equiv "
%% ODER: format /=         = "\neq "
%format <=         = "\leq "
%format >=         = "\geq "
%format `elem`     = "\in "
%format `notElem`  = "\notin "
%format &&         = "\mathrel{\wedge}"
%format ||         = "\mathrel{\vee}"
%format >>         = "\sequ "
%format >>=        = "\bind "
%format $          = "\mathbin{\$}"
%format `seq`      = "\mathbin{\Varid{`seq`}}"
%format !          = "\mathbin{!}"
%format //         = "\mathbin{//}"
%format undefined  = "\bot "
%format not	   = "\neg "
%if meta
%format M.a = "a"
%format M.b = "b"
%format M.c = "c"
%format M.d = "d"
%format M.e = "e"
%format M.f = "f"
%format M.g = "g"
%format M.h = "h"
%format M.i = "i"
%format M.j = "j"
%format M.k = "k"
%format M.l = "l"
%format M.m = "m"
%format M.n = "n"
%format M.o = "o"
%format M.p = "p"
%format M.q = "q"
%format M.r = "r"
%format M.s = "s"
%format M.t = "t"
%format M.u = "u"
%format M.v = "v"
%format M.w = "w"
%format M.x = "x"
%format M.y = "y"
%format M.z = "z"
%format M.A = "A"
%format M.B = "B"
%format M.C = "C"
%format M.D = "D"
%format M.E = "E"
%format M.F = "F"
%format M.G = "G"
%format M.H = "H"
%format M.I = "I"
%format M.J = "J"
%format M.K = "K"
%format M.L = "L"
%format M.M = "M"
%format M.N = "N"
%format M.O = "O"
%format M.P = "P"
%format M.Q = "Q"
%format M.R = "R"
%format M.S = "S"
%format M.T = "T"
%format M.U = "U"
%format M.V = "V"
%format M.W = "W"
%format M.X = "X"
%format M.Y = "Y"
%format M.Z = "Z"
%format M.alpha   = "\alpha "
%format M.beta    = "\beta "
%format M.gamma   = "\gamma "
%format M.delta   = "\delta "
%format M.epsilon = "\epsilon "
%format M.zeta    = "\zeta "
%format M.eta     = "\eta "
%format M.theta   = "\theta "
%format M.iota    = "\iota "
%format M.kappa   = "\kappa "
%format M.lambda  = "\lambda "
%format M.mu      = "\mu "
%format M.nu      = "\nu "
%format M.xi      = "\xi "
%format M.pi      = "\pi "
%format M.rho     = "\rho "
%format M.sigma   = "\sigma "
%format M.tau     = "\tau "
%format M.upsilon = "\upsilon "
%format M.phi     = "\phi "
%format M.chi     = "\chi "
%format M.psi     = "\psi "
%format M.omega   = "\omega "
%format M.Gamma   = "\Gamma "
%format M.Delta   = "\Delta "
%format M.Theta   = "\Theta "
%format M.Lambda  = "\Lambda "
%format M.Xi      = "\Xi "
%format M.Pi      = "\Pi "
%format M.Sigma   = "\Sigma "
%format M.Upsilon = "\Upsilon "
%format M.Phi     = "\Phi "
%format M.Psi     = "\Psi "
%format M.Omega   = "\Omega "
%format M.forall  = "\forall "
%format M.exists  = "\exists "
%format M.not     = "\neg "
%format ==>       = "\enskip\Longrightarrow\enskip "
%format <==       = "\enskip\Longleftarrow\enskip "
%format /\        = "\enskip\mathrel{\wedge}\enskip "
%format \/        = "\enskip\mathrel{\vee}\enskip "
%format M.=       = "="
%format M./=      = "\neq "
%format M.<       = "<"
%format M.<=      = "\leq "
%format M.>=      = "\geq "
%format M.>       = ">"
%endif
%endif