[Agda] lhs2tex and with

[Dan Licata]

Thanks!

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).    

-Dan

On Oct27, kahl at cas.mcmaster.ca wrote:
> 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
>