[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