Skip to content

fix: alias respects noncomputable section and opens namespace prefix#1906

Open
Chessing234 wants to merge 3 commits into
leanprover-community:mainfrom
Chessing234:fix/alias-noncomputable-section-and-namespace
Open

fix: alias respects noncomputable section and opens namespace prefix#1906
Chessing234 wants to merge 3 commits into
leanprover-community:mainfrom
Chessing234:fix/alias-noncomputable-section-and-namespace

Conversation

@Chessing234

@Chessing234 Chessing234 commented Jul 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

  • alias in a noncomputable section inherits noncomputable and marks the synonym (#1097).
  • Namespaced alias Foo.bar := x opens Foo when resolving x, matching def (#810).

Fixes #810
Fixes #1097

Test plan

  • lake build BatteriesTest.alias
  • lake build BatteriesTest.alias_module
  • CI (awaiting fork workflow approval)

awaiting-review

@github-actions github-actions Bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Jul 16, 2026
@Chessing234

Chessing234 commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

awaiting-review

@github-actions github-actions Bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Jul 16, 2026
@Chessing234 Chessing234 mentioned this pull request Jul 17, 2026
Open
Chessing234 and others added 2 commits July 17, 2026 08:56
@Chessing234 @cursoragent
fix: alias respects noncomputable section and opens namespace prefix
8267675 
Co-authored-by: Cursor <cursoragent@cursor.com>
@Chessing234 @cursoragent
fix: keep public alias of private def rejection
26bd057 
resolveAliasTarget must not always run withoutExporting;
the second resolve for defs needs the caller's export scope.

Co-authored-by: Cursor <cursoragent@cursor.com>
@Chessing234
Chessing234 force-pushed the fix/alias-noncomputable-section-and-namespace branch from 30c7f31 to 26bd057 Compare July 17, 2026 05:58
@Chessing234

Chessing234 commented Jul 17, 2026

Copy link
Copy Markdown
Contributor Author

Pushed a follow-up: resolveAliasTarget no longer always uses withoutExporting, so public aliases of private defs still get rejected (fixes the alias_module guard). CI is waiting on workflow approval for the fork push.

@YaelDillies

YaelDillies commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

Can you mark this as fixing #810 and #1097?

@Chessing234

Chessing234 commented Jul 17, 2026

Copy link
Copy Markdown
Contributor Author

Done — PR body now has Fixes #810 and Fixes #1097.

@mathlib-nightly-testing

mathlib-nightly-testing Bot commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

Mathlib CI status (docs):

mathlib-nightly-testing Bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 25, 2026
@mathlib-nightly-testing
Trigger CI for leanprover-community/batteries#1906
19801b5
@mathlib-nightly-testing

mathlib-nightly-testing Bot commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

Mathlib CI status (docs):

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

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review This PR is ready for review; the author thinks it is ready to be merged. breaks-mathlib

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

alias ignores noncomputable section alias does not open namespaces

3 participants

@Chessing234 @YaelDillies @fgdorais