[Agda] Bug in ScopeMonad?

[Nils Anders Danielsson]

On 2012-06-25 21:26, Paul van der Walt wrote:
> PS: assuming the code gets cleaned up a little, is this a
> feature others would use? I'm finding it a huge time-saver.

Sounds useful, yes.

Unfortunately the spacing around underscores is often not what I want,
so I tend to end up with formatting rules like the following:

   %format _∷_   = "{" _ "\mkern1mu"    ∷    "\mkern-1mu"   _ "}"
   %format _≡_   = "{" _ "\mkern0.8mu"  ≡    "\mkern-1mu"   _ "}"
   %format _>>=_ = "{" _ "\mkern-0.5mu" >>=  "\mkern-2.1mu" _ "}"

If someone knows a way around this I would very much like to hear about
it.

-- 
/NAD