[isabelle-dev] locales, groups, metric spaces?
lp15 at cam.ac.uk
Mon Apr 15 11:57:02 CEST 2019
In the context of the recent discussions about Algebra, we could revisit these issues in the context of metric spaces, which we still don’t have (except as type classes). A metric space has a carrier and a binary relation, so syntactically it’s similar to a monoid, except that we don’t expect to extend one with additional fields. So, at least, we should be able to avoid records.
But what about the path from metric spaces to normed vector spaces, etc.?
More information about the isabelle-dev