zstone1

A question about prioritizing this work. It's possible to do this while we do the port to HB. However, doing it the traditional module theory way will require defining a...

Ah, that is not surprising. I guess everyone is waiting for scala 3 to do any real maintenance. Well, with no obvious path forward, I'll see about downgrading the other...

Yeah, there's no silver bullet as I suspected. I had thought about the dependent typing issues, and it's not nice. Is there even a decision procedure for vector arithmetic? Certainly...

Yeah, I'm seeing it work well. There are a couple interesting consequences of this approach: 1. If `(f : subspace A -> T)` in the first place, then `continuous f`...

There are a lot of places where this notation will be used, and a lot of different use cases and requirements we've encountered. So I'd like to start by just...

This issue is now duplicate of the above ticket in filed in HB repo.

I'm very happy to see more specialized convergences. I will propose an alternate approach: to build a topology on `{RV P >-> R}` that induces this convergence. This is the...

As an aside, today I was quite surprised to learn that "almost everywhere convergence" is [not topological](http://ordman.net/MathResearch/1966A.pdf). So while it looks like we could define a "filteredType" for it, we...

I see. Fascinating. Naively, I would not have expected the order of instance declarations to ever matter. Although with your explanation I do see how that happened. An error message...

FYI, I've merged several results (metrics for supremums and quotients) in the last few days that involve some mixins. Just a heads up to A) Expect the rebase of topology.v...