Owen Lynch
Owen Lynch
is this likely to happen any time soon, given that this issue has been open for a year and the last commit on this repo was in january?
Oh shoot! I totally didn't see this @MasonProtter. I will look at it now.
OK, I understand what this is doing now. I have to integrate it a little with some unpushed work, but hopefully I can merge this today. Sorry, I almost never...
@MasonProtter I'm so sorry this took so long; thank you for the PR! I should be more responsive now; I was finishing my thesis May-July, and I've now started working...
Sorry for taking a while to get back to this; I'm just now opening up my laminar project again. The problem is that I'm worried that that the following code...
OK, this is actually fine though, because I could actually wrap this in a future and then pass `b` into the callback. This is already inside of some async stuff,...
I made isnormalsubgr into a `hProp`, and fixed up the style of my proofs. Couple questions: It would be nice to have cosets as objects that I could work with,...
My impression of the definition of weak equivalence for subtypes is that it should be pretty easily implied by my lcoset_equals_rcoset type, as long as lcoset and rcoset are suitably...
Yeah, that was the definition that I was thinking of.
In the `@theory` macro, could we generate an abstract type representing maps between instances of the theory that only made you define the map on generators? Alternatively, we could write...