-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore(linear_algebra): rename type variables #1521
Conversation
I've just updated |
src/linear_algebra/basic.lean
Outdated
@@ -56,303 +56,305 @@ open function lattice | |||
reserve infix ` ≃ₗ `:25 | |||
|
|||
universes u v w x y z | |||
variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type y} {ε : Type z} {ι : Type x} | |||
variables {R κ : Type u} {M V : Type v} {M₂ V₂ : Type w} {M₃ V₃ : Type y} {M₄ : Type z} {ι : Type x} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why are there variables in the same universe, instead of one universe for each variable? This seems to be calling for trouble...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They should never mix. R
replaced α
in module defs/theorems, κ
for vector spaces.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Until someone writes in this file a statement with R
and κ
and doesn't pay attention to the fact that they belong to the same universe...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, fair enough. I was thinking in terms of faithfully translating the old file. Updated -- this should be safe in both respects.
I think the only outstanding issue here is that we're not standardized on |
FWIW I prefer |
I don't think we really care. In the analysis folder, switching to |
This change is not 100% syntactic. The order of arguments seems to be permuted in six declarations. As far as we can tell, this is all that's happened, there are no unified universe levels. So I'll merge now, and note the alpha-normalized diff here (thanks @rwbarton ) for future reference.
|
* doc(linear_algebra/basis): add doc * doc(linear_algebra/basis): shorten docstrings * refactor(linear_algebra/basis): rename type vars * style(linear_algebra/basic): change variable names * chore(linear_algebra/dimension): rename type variables * remove commented code * style(linear_algebra/bilinear_form): change variable names * style(linear_algebra/direct_sum_module): change variable names * style(linear_algebra/matrix): change variable names * Rename variables in finsupp_vector_space.lean * style(linear_algebra/sesquilinear_form): change variable names * style(linear_algebra/tensor_product): change variable names * change kappas to bb k's * style(linear_algebra/finsupp): change variable names * change universe levels * change bb k to K
Rename the type variables in linear algebra from greek letters to
R
for rings𝕜
for fieldsM
for modulesV
/E
for vector spaces