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: `@[simp]` removed #11119

Open

pitmonticone opened this issue Mar 2, 2024 · 0 comments

Labels

Collaborator

pitmonticone commented Mar 2, 2024 •

edited

Classifies porting notes claiming anything semantically equivalent to:

"@[simp] removed [...]"
"@[simp] removed [...]"
"removed simp attribute"

Related to: #10618

Examples

mathlib4/Mathlib/Order/WellFounded.lean

Lines 230 to 234 in e6232b7

    
           --Porting note: @[simp] removed as it will never apply 
        
           theorem argminOn_le (s : Set α) {a : α} (ha : a ∈ s) (hs : s.Nonempty := Set.nonempty_of_mem ha) : 
        
               f (argminOn f h s hs) ≤ f a := 
        
             not_lt.mp <| not_lt_argminOn f h s ha hs 
        
           #align function.argmin_on_le Function.argminOn_le

mathlib4/Mathlib/Data/Prod/Basic.lean

Lines 100 to 104 in e6232b7

    
           -- Porting note: `@[simp]` tag removed because auto-generated `mk.injEq` simplifies LHS 
        
           -- @[simp] 
        
           theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ := 
        
             Iff.of_eq (mk.injEq _ _ _ _) 
        
           #align prod.mk.inj_iff Prod.mk.inj_iff

mathlib4/Mathlib/Data/Multiset/Bind.lean

Lines 222 to 226 in e6232b7

    
           -- Porting note: @[simp] removed because not in normal form 
        
           theorem attach_bind_coe (s : Multiset α) (f : α → Multiset β) : 
        
               (s.attach.bind fun i => f i) = s.bind f := 
        
             congr_arg join <| attach_map_val' _ _ 
        
           #align multiset.attach_bind_coe Multiset.attach_bind_coe

The text was updated successfully, but these errors were encountered:

pitmonticone added the porting-notes label

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify @[simp] removed porting notes #11121

Closed

jcommelin mentioned this issue

Porting note: simp / @[simp] can prove it #10618

Open

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

26c7c0e

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

3e6dab6

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify @[simp] removed porting notes #11184

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

28527d3

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

kbuzzard pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

fc6b4f8

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

kbuzzard pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

3e0c081

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

dagurtomas pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

8dcbca5

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

dagurtomas pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

4f336f0

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

semorrison mentioned this issue

tracking issue for change in behaviour in @[simp] def #11647

Open

utensil pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

7c9e865

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

utensil pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

Louddy pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11121)

ac2a63c

Classifies by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `@[simp]`"

Louddy pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

664f89f

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

callesonne pushed a commit that referenced this issue


          chore: classify @[simp] removed porting notes (#11184)

93ef20c

Classifying by adding issue number #11119 to porting notes claiming anything semantically equivalent to: 

- "`@[simp]` removed [...]"
- "@[simp] removed [...]"
- "removed `simp` attribute"

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