search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.51k stars 332 forks source link

Porting note: TODO #11215

Open pitmonticone opened 8 months ago

pitmonticone commented 8 months ago

Classifies porting notes claiming "TODO".

We might need some subclassification at a later stage.

Examples

https://github.com/leanprover-community/mathlib4/blob/7e0bc5a7c6c4304480f2fafe0408a1edd536a679/Mathlib/Analysis/Normed/Group/Quotient.lean#L407-L412

https://github.com/leanprover-community/mathlib4/blob/7e0bc5a7c6c4304480f2fafe0408a1edd536a679/Mathlib/Data/Analysis/Filter.lean#L25-L35

https://github.com/leanprover-community/mathlib4/blob/7e0bc5a7c6c4304480f2fafe0408a1edd536a679/Mathlib/Data/ENNReal/Operations.lean#L70-L78

https://github.com/leanprover-community/mathlib4/blob/7e0bc5a7c6c4304480f2fafe0408a1edd536a679/Mathlib/Geometry/Manifold/Diffeomorph.lean#L473-L478

grunweg commented 6 months ago

A few notes classified here are actually instances of #5171.