Jacques Carette
Jacques Carette
It might be an Agda issue, I don't know. I was asking for a separate issue where we could track our findings. The current issues are appropriately focused on getting...
I should also link in #2287 "Mechanize the Algebra hierarchy". I think that the design space for both are quite similar and should likely have a similar solution.
Yes, definitely need to look at FREX and its idris implementation. All these ponderings have made me realize one thing: we already have, at least, all of "FreeMonoid" already implemented...
Thanks for posting this. For reporting upstream, we'll have to golf a bit to get a MWE that eliminates as much stdlib as possible by inlining.
I agree that we shouldn't hold up v2.1 for this.
Strong YES from me. Not only is your reasoning sound, one can also witness that Agda is used a lot by people doing PL meta-theory. We should strive to make...
Sigh - another case where metaprogramming would probably be a reasonable solution. I've been having many discussions (with @TOTBWF ) about how I think we ought to be able to...
Could you augment your report with more details than "doesn't work"? Hard error or yellow or does not terminate or .... ?
While it "makes sense" to add `IsBooleanRing` to `Algebra.Lattice.Structures.Biased`, it also pretty much insures no one's going to find it... `IsBooleanRing` in my mind is part of the 'usual' `Algebra`...
Much hesitation on this. I'm sure we could muddle through sensibly for `BooleanRing`, but that's just the tip of the iceberg. I wouldn't want to set the wrong precedent here...