Qiyuan Xu (Mar 31 2022 at 04:25): Qiyuan Xu (Mar 31 2022 at 04:25):Hi, I read the tutorial on locales. It gives examples like lattice_hom which is great and looks general, so I naturally think there should be locales like plus_homomoprhism and group_homomoprhism in the standard library, but I didn't find them. Did I find at wrong places? Or, is there any particular reason to not include such locales in the standard library?
Manuel Eberl (Apr 07 2022 at 11:33):I agree that these things would be a good idea, but no, I'm also not aware of them…
Manuel Eberl (Apr 07 2022 at 11:33):maybe somebody else can pitch in?
Manuel Eberl (Apr 07 2022 at 11:33):perhaps also a good idea to ask on the mailing list
Manuel Eberl (Apr 07 2022 at 11:33):more people might comment there
Last updated: Dec 30 2024 at 16:22 UTC