[Agda] Sane whitespace with agda --latex

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Sat Apr 25 18:46:17 CEST 2015


Hi,

It seems that agda --latex gives a result with horizontal whitespace
that often doesn't resemble the source file. Sometimes things like

foo : Bar x
          y
          z

will be turned into

foo : Bar x
      y
      z

Sometimes stuff like

x      : a -> b
longer : a -> b
foo    : a -> b

Results in some things being properly aligned and others not.

I even had a case of

foo : x
    -> let bar : a -> b
     bar = …
       in …

Is there any way to generate whitespace that's consistent with the
source document? I'm not using tabs or anything like that.


-- 
Mateusz K.


More information about the Agda mailing list