[Agda] lhs2tex and with
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Thu Oct 28 12:30:37 CEST 2010
On 2010-10-27 23:50, Dan Licata wrote:
> That works, as long as you line up the |'s with the w of the with,
> rather than the h (otherwise they get left-justified, but the patterns
> are fine in any case).
You can use a format directive to insert a suitable amount of space
before the vertical bars:
%format | = "\mkern???mu|"
Maybe the following would also work, I haven't tested:
%format | = "\phantom{" with "}\mkern-???mu|"
You can limit the scope of a format directive by using %{ ... %}.
--
/NAD
More information about the Agda
mailing list