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: added `instance` #10754

Open

pitmonticone opened this issue Feb 20, 2024 · 0 comments

Labels

Collaborator

pitmonticone commented Feb 20, 2024 •

edited

Classifies porting notes claiming anything semantically equivalent to:

"added instance"
"new instance"
"adding instance"
"had to add this instance manually"

Examples

mathlib4/Mathlib/RingTheory/Valuation/ValuationSubring.lean

Lines 309 to 316 in 4c3321a

    
           instance ofPrime_scalar_tower (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] : 
        
               -- Porting note: added instance 
        
               letI : SMul A (A.ofPrime P) := SMulZeroClass.toSMul 
        
               IsScalarTower A (A.ofPrime P) K := 
        
             IsScalarTower.subalgebra' A K K 
        
               -- Porting note: filled in the argument 
        
               (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors) 
        
           #align valuation_subring.of_prime_scalar_tower ValuationSubring.ofPrime_scalar_tower

mathlib4/Archive/Arithcc.lean

Lines 252 to 254 in 4c3321a

    
           -- Porting note: added 
        
           instance (t : Register) : Trans (StateEq (t + 1)) (StateEq (t + 1)) (StateEq (t + 1)) := 
        
             ⟨@StateEq.trans _⟩

mathlib4/Archive/Arithcc.lean

Lines 264 to 266 in 4c3321a

    
           -- Porting note: added 
        
           instance (t : Register) : Trans (StateEq (t + 1)) (StateEqRs (t + 1)) (StateEqRs (t + 1)) := 
        
             ⟨@StateEqStateEqRs.trans _⟩

pitmonticone added the porting-notes label

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify added instance porting notes #10755

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10755)

283cf08

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify added instance porting notes #10884

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

45fab6c

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

thorimur pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10755)

7fa17b3

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

thorimur pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

ccd72e5

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify added instance porting notes #10925

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10925)

1d96f99

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

thorimur pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10755)

3b3a7e5

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

thorimur pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

b967438

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify added instance porting notes #11085

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

8f422f3

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

riccardobrasca pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10755)

a3cbdf6

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

riccardobrasca pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

39ed3ed

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

riccardobrasca pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10925)

68b1567

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

riccardobrasca pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

00027df

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

kbuzzard pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

c381887

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

pitmonticone mentioned this issue

[Merged by Bors] - chore: classify new instance porting notes #11433

Closed

mathlib-bors bot pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

Classifies by adding issue number #10754 to porting notes claiming "new instance".

dagurtomas pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10755)

4b8a18f

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

dagurtomas pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

b002c67

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

dagurtomas pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10925)

97dd9ae

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

dagurtomas pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

bd2520f

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

dagurtomas pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

44f4706

Classifies by adding issue number #10754 to porting notes claiming "new instance".

utensil pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

fa9bff4

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

utensil pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

c7129b2

Classifies by adding issue number #10754 to porting notes claiming "new instance".

Louddy pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10884)

4fc9f61

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

Louddy pushed a commit that referenced this issue


          chore: classify added instance porting notes (#10925)

3ca0c05

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.

Louddy pushed a commit that referenced this issue


          chore: classify added instance porting notes (#11085)

1c3b434

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

- "added instance"
- "new instance"
- "adding instance"
- "had to add this instance manually"

Louddy pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

812a8fe

Classifies by adding issue number #10754 to porting notes claiming "new instance".

atarnoam pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

f22bad9

Classifies by adding issue number #10754 to porting notes claiming "new instance".

uniwuni pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

c7325e4

Classifies by adding issue number #10754 to porting notes claiming "new instance".

callesonne pushed a commit that referenced this issue


          chore: classify new instance porting notes (#11433)

7a27d47

Classifies by adding issue number #10754 to porting notes claiming "new instance".

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