[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