Skip to content

minor generalization and renaming#1443

Merged
affeldt-aist merged 1 commit intomath-comp:masterfrom
affeldt-aist:measure_20241227
Dec 29, 2024
Merged

minor generalization and renaming#1443
affeldt-aist merged 1 commit intomath-comp:masterfrom
affeldt-aist:measure_20241227

Conversation

@affeldt-aist
Copy link
Member

Motivation for this change

there was a useless dependency of the measurable_?section lemmas on a realType
this PR also performs some renamings, favoring set_system instead of class @t6s

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Dec 27, 2024
@affeldt-aist affeldt-aist added this to the 1.9.0 milestone Dec 27, 2024
@affeldt-aist affeldt-aist merged commit 155492b into math-comp:master Dec 29, 2024
ndslusarz pushed a commit to ndslusarz/analysis that referenced this pull request Feb 12, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

renaming/refactoring 🔧 This is about a renaming or refactoring in the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant