[Agda] lhs2tex and with

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Wed Oct 27 23:48:19 CEST 2010


Dan,

 > lhs2TeX --agda is quite nice.  One question, though: I often format
 > 'with' code so that the branches line up with the scrutinee:
 > 
 > f x y with z
 > ...      | p1 = ...
 > ...      | p2 = ...
 > 
 > Are there any tricks to get lhs2TeX to keep this formatting? It seem to
 > left-justify the branches.  

General lhs2TeX rule:
Anything aligned after two or more spaces remains aligned.
Therefore, the following should work better:


f x y  with  z
...       |  p1 = ...
...       |  p2 = ...

     ^^    ^^


Wolfram


More information about the Agda mailing list