You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The parentheses are in most cases a little further out than they need to be. Here's one example where it looks really odd:
Sometimes extra horizontal whitespace is inserted even when in an AgdaSuppressSpace environment. Here's an example:
For the first case, I think it's best if we just make all the parentheses sit a little closer. For the second case, I assume there is some bug that generates an extra line somehow?
The text was updated successfully, but these errors were encountered:
There are two separate issues here:
AgdaSuppressSpace
environment. Here's an example:For the first case, I think it's best if we just make all the parentheses sit a little closer. For the second case, I assume there is some bug that generates an extra line somehow?
The text was updated successfully, but these errors were encountered: