[Agda] Sane whitespace with agda --latex

[Wolfram Kahl]

On Mon, Apr 27, 2015 at 10:10:42AM +0100, Mateusz Kowalczyk wrote:
> On 04/26/2015 05:20 PM, Andreas Abel wrote:
> > As far as I know, to get alignment you need two spaces.
> > 
> > foo : Bar  x
> >             y
> >             z
> > 
> > (Otherwise, how could unintended alignment be ruled out?)
>
> I tried this and it made no difference. Further, such a hack won't work
> for inside let.

That would be another reason to stick with lhs2TeX:

   http://www.andres-loeh.de/lhs2tex/

(Reading the manual is necessary. The two-space rule essentially
 comes from there. With my Emacs setup, Unicode characters like
 suffix _1 etc. do not have the same width as other characters,
 so frequently it is necessary to look at the column numbers
 in the status bar to be able to actually achieve alignment.)

My main reason to not even consider ``agda --latex'' right now
is that, as far as I know (and I do read Agda release notes),
it does not typeset in-line code (as in ``|sym D.Laws A.assoc|'').
I find that even a minimal degree of literacy is hard to achieve
without the facility to typeset in-line code.


> I end up with having ugly sections like at
> http://fuuzetsu.co.uk/images/1430125773.png .

(Too much is missing from that picture to even guess what you might
 want to point to.)



Wolfram