Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Porting note: removed @[pp_nodot] #11180

Closed
pitmonticone opened this issue Mar 5, 2024 · 0 comments
Closed

Porting note: removed @[pp_nodot] #11180

pitmonticone opened this issue Mar 5, 2024 · 0 comments
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.

Comments

@pitmonticone
Copy link
Collaborator

pitmonticone commented Mar 5, 2024 •
edited
Loading

Classifies porting notes claiming:

removed @[pp_nodot]

Examples

mathlib4/Mathlib/Algebra/Symmetrized.lean

Lines 48 to 57 in 2a65c8d

/-- The element of `SymAlg α` that represents `a : α`. -/
@[match_pattern]
-- Porting note: removed @[pp_nodot]
def sym : α ≃ αˢʸᵐ :=
Equiv.refl _
#align sym_alg.sym SymAlg.sym
/-- The element of `α` represented by `x : αˢʸᵐ`. -/
-- Porting note: removed @[pp_nodot]
def unsym : αˢʸᵐ ≃ α :=

@pitmonticone pitmonticone added the porting-notes Mathlib3 to Mathlib4 porting notes. label Mar 5, 2024
@pitmonticone pitmonticone mentioned this issue Mar 5, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Mar 5, 2024
@pitmonticone
chore: classify removed @[pp_nodot] porting notes (#11181)
76aa1eb 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
kbuzzard pushed a commit that referenced this issue Mar 12, 2024
@pitmonticone @kbuzzard
chore: classify removed @[pp_nodot] porting notes (#11181)
c30fa3d 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
@pitmonticone pitmonticone mentioned this issue Mar 17, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Mar 17, 2024
@pitmonticone
chore: classify "removed @[pp_nodot]" porting notes (#11447)
d706fb5 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@pitmonticone @dagurtomas
chore: classify removed @[pp_nodot] porting notes (#11181)
1463213 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@pitmonticone @dagurtomas
chore: classify "removed @[pp_nodot]" porting notes (#11447)
aec03d9 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
utensil pushed a commit that referenced this issue Mar 26, 2024
@pitmonticone @utensil
chore: classify removed @[pp_nodot] porting notes (#11181)
33c9adb 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
utensil pushed a commit that referenced this issue Mar 26, 2024
@pitmonticone @utensil
chore: classify "removed @[pp_nodot]" porting notes (#11447)
0cfdbe0 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
Louddy pushed a commit that referenced this issue Apr 15, 2024
@pitmonticone @Louddy
chore: classify removed @[pp_nodot] porting notes (#11181)
2e8289b 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
Louddy pushed a commit that referenced this issue Apr 15, 2024
@pitmonticone @Louddy
chore: classify "removed @[pp_nodot]" porting notes (#11447)
c763391 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
atarnoam pushed a commit that referenced this issue Apr 16, 2024
@pitmonticone @atarnoam
chore: classify "removed @[pp_nodot]" porting notes (#11447)
f783a63 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
uniwuni pushed a commit that referenced this issue Apr 19, 2024
@pitmonticone @uniwuni
chore: classify "removed @[pp_nodot]" porting notes (#11447)
522310e 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
callesonne pushed a commit that referenced this issue Apr 22, 2024
@pitmonticone @callesonne
chore: classify removed @[pp_nodot] porting notes (#11181)
cd163bb 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
callesonne pushed a commit that referenced this issue Apr 22, 2024
@pitmonticone @callesonne
chore: classify "removed @[pp_nodot]" porting notes (#11447)
e0e36cd 
Classifies by adding issue number #11180 to porting notes claiming: 

> removed `@[pp_nodot]`
kmill added a commit that referenced this issue Jun 12, 2024
@kmill
chore: address @[pp_nodot] porting notes
6dc73fa 
closes #11180
@kmill kmill mentioned this issue Jun 12, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Jun 24, 2024
@kmill
chore: address @[pp_nodot] porting notes (#13781)
ae381af 
Adds in `@[pp_nodot]` wherever there was a porting note, except in some cases where by principle it can never have an affect (such as for `MulOpposite.op` or `SymAlg.sym`).

closes #11180
@mathlib-bors mathlib-bors bot closed this as completed in 669326e Jun 24, 2024
kbuzzard pushed a commit that referenced this issue Jun 26, 2024
@kmill @kbuzzard
chore: address @[pp_nodot] porting notes (#13781)
dfb56c2 
Adds in `@[pp_nodot]` wherever there was a porting note, except in some cases where by principle it can never have an affect (such as for `MulOpposite.op` or `SymAlg.sym`).

closes #11180
dagurtomas pushed a commit that referenced this issue Jul 2, 2024
@kmill @dagurtomas
chore: address @[pp_nodot] porting notes (#13781)
6125967 
Adds in `@[pp_nodot]` wherever there was a porting note, except in some cases where by principle it can never have an affect (such as for `MulOpposite.op` or `SymAlg.sym`).

closes #11180
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Merged by Bors] - chore: address @[pp_nodot] porting notes leanprover-community/mathlib4
1 participant
@pitmonticone