[isabelle-dev] locales, groups, metric spaces?

[Lawrence Paulson]

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.?

Larry