G. Allais

> Regarding Box and Diamond syntax... I realise we don't have these (-monotone/functorial in each argument!) definitions in full generality for R : REL A B _, where they're usually...

FTR, these cannot be turned into `where` definitions because these get lifted to the toplevel and that is not done in a modality-respecting way. In other words: turning these into...

I would argue in favour of mandatory explicit import lists if they mention, say, max half a dozen identifiers. Throwing these in as we touch modules should hopefully help us...

I'm not married to v2.0, I think I just picked version numbers based on what I saw listed on [the ghc download page of each version](https://www.haskell.org/ghc/download.html). Looking at the README,...

One of the design decisions of this library is that all the Parsers you can define *have* to consume some of their input. This makes deciding whether it is safe...

Alternatively, because there is no real control flow dependency between the value of `x` and the parser that gets run afterwards, you could have: ```coq Definition float_Q_cast (x : N)...

Nice! This is what I'd do: ```coq Definition float_Q_cast : (Z * option (NEList ascii) * N) -> Q := fun '((x , zeros) , z) => Qmake x (match...

> I imagine that one would somehow like to compare with the stdlibs of ocaml and haskell. It's probably also worth looking at the ones for other theorem provers. See...

If you make sure that *all* `_,_` have the same fixity level then it should fix the issue, I believe.

Is there a use-case where you'd want to not export a function in Haskell but you'd be happy to export it in Agda? Otherwise using `private` blocks as a way...