Skip to content

Conversation

@robsimmons
Copy link
Contributor

Following up from a conversation with @david-christiansen about "field projection" being confusing in the case of generalized field notation.

Proposed guideline:

Generalized field notation does not introduce new projections: a.x is (generalized) field notation, a.1 is a projection or projection notation. If .x is an invocation of a function that is not a part of the structure, then it is a, .x is a field access. If x is an actual declared part of the structure that could equivalently be projected with projection notation, then .x may be referred to as a projection or field projection. (Field access is the more general term.)

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 6, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-06 16:21:50)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-06 16:21:51)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants