Open carlostome opened 6 years ago
This looks like a real bug, unfortunately.
A workaround might be to define
%format (abs (a)) = "\mathopen{|}" a "\mathclose{|}"
instead and then
abs(1) = (abs(2))
I suspect that even =
is considered by the lhs2tex Agda lexer as a valid argument, so that the whole line is parsed as the first abs
being applied to four arguments ...
Compiling the following code,
with
lhs2TeX --poly
produces the expected result,|1| = |2|
, whereaslhs2TeX --agda
does not recognize the argument to the second use ofabs
producing|1| = |.| (2)
.