Matthew Daggitt

Thanks for the reply @andreasabel. So, without making keywords such as `let` a token, what is the procedure to extract the location of the `let` expression in the source code...

That would certainly address our current problems. I can't help but wonder though if it's a bit hacky though, for example you would have to pattern match on the list...

@sstucki reviewing this PR has triggered a shift in my thinking about the design of the library. All of your questions result from there being no natural place to put...

Apologies for the delay in replying. > I think I lack imagination for the meaning of algebra-construct-natural-choice. Is natural choice a mathematical concept around orders? Is there even a choice...

Hi @TOTBWF, yup agreed these definitions are super-hard to work with. Because of that, we're in the process of trying to define a more useable function hierarchy (see `Function.Structures/Bundles`) and...

> I'm not sure where this should live or how it should look, however. Well the principled place would be `Function.Relation.Binary.Pointwise` and `Function.Relation.Binary.Equality`...

> I did not notice that Data.Char defines a bunch of relations which, in other parts, are done in separate sub-modules Hmm so I don't think that this is inconsistent...

So concretely you'd be proposing turning the definition of `RawIApplicativeZero` into the following? ```agda record RawIApplicativeZero {I : Set i} (F : IFun I f) : Set (i ⊔ suc...

We're planning to reorganise `Effect.Functor` etc. in v2.0 and will come back to this after this...

Okay so I agree `unfold` is nicer than `defn` :+1: But I think that definition of `unfold-reverse` shouldn't be called either variant, as it's not really unfolding `reverse`, it's instead...