Andre Knispel

I think it would be nice to have that as a third option for `mouse_follows_focus`, as I think it would be a good default. `mouse_follows_focus on` can be pretty annoying...

This is intended behaviour, if you check the spec that it will also fail in this situation. The reason is that we want to ensure that the block producer can...

Adding as well as removing scripts should be impossible, i.e. we want the set of scripts to be specified exactly. If we allowed scripts to be both present in the...

Yes, that's what it is about. It's not really that we think there's an attack, or that it's particularly bad if something changed that doesn't affect anything, it's just that...

Thanks! We're currently in the process of doing an internal audit, and I think all of these points except for the typo in 4.2 are already fixed or on my...

We agreed yesterday that moving all the names like `_+_, map`, etc. that would clash with type classes (and that do clash with other modules right now) into a separate...

> Err I'm afraid I'm not quite sure that's what I got. I thought that the conclusion was that we should have a separate module that imported everything you need...

It seems that this is indeed not the fault of `reduce`. I changed `test` to this: ``` agda test : TC ⊤ test = let t = def₁ (quote f)...

In my opinion, the current system of `unquoteDecl` and `unquoteDef` is very limiting and I think there's a different direction to go in that would also make this a non-issue....

`Monad.lidr` is also incredibly slow to compile for me. Is it known what makes these things slow?