pseudometric alias #1628
Merged
pseudometric alias #1628
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
affeldt-aist
force-pushed
the
normed_20250522
branch
from
90a04b1 to
aced715
Compare
Tragicus
reviewed
Jun 4, 2025
| End numFieldNormedType. | ||
| Import numFieldNormedType.Exports. | ||
|
|
||
| Definition pseudoMetric_normed (K : numFieldType) (M : normedZmodType K) : Type |
Collaborator
There was a problem hiding this comment.
Is there not pseudometric somewhere? If so, why do we need to change the alias?
Member
Author
There was a problem hiding this comment.
I looked at existing aliases (e.g., pseudoMetric_bool in bool_topology.v) and observed that they had more elaborated names, so I concluded that a name that better explains the input and the output could be more appropriate, hence the name change.
Member
Author
There was a problem hiding this comment.
arg, not a good example since this precise example might actually be useless, see issue #1636
Co-authored-by: Quentin Vermande <[email protected]>
Tragicus
approved these changes
Jun 5, 2025
affeldt-aist
added
the
enhancement ✨
IshiguroYoshihiro
pushed a commit
to IshiguroYoshihiro/analysis
that referenced
this pull request
Jun 12, 2025
* alias for pseudometric and factory for normed module --------- Co-authored-by: Quentin Vermande <[email protected]>
IshiguroYoshihiro
pushed a commit
to IshiguroYoshihiro/analysis
that referenced
this pull request
Jun 20, 2025
* alias for pseudometric and factory for normed module --------- Co-authored-by: Quentin Vermande <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Motivation for this change
fixes #1636
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers