Zulip Chat Archive

Stream: mathlib4

Topic: !4#2832

Jeremy Tan (Mar 12 2023 at 20:27):

!4#2831 I've got a little more experience now, but there's one error I can't seem to fix (for the moment), can somebody take a look?

Jeremy Tan (Mar 12 2023 at 20:28):

It's in raiseCone

Adam Topaz (Mar 12 2023 at 20:42):

@[simps]
def raiseCone [IsConnected J] {B : C} {F : J ⥤ Over B} (c : Cone (F ⋙ forget B)) :
    Cone F where
  pt := Over.mk (c.π.app (Classical.arbitrary J) ≫ (F.obj (Classical.arbitrary J)).hom)
  π :=
    { app := fun j =>
        Over.homMk (c.π.app j) (nat_trans_from_is_connected (c.π ≫ natTransInOver F) j _)
      naturality := by
        intro X Y f
        apply CommaMorphism.ext
        · simpa using (c.w f).symm
        · simp }

Jeremy Tan (Mar 12 2023 at 21:12):

Now the linter revealed an unused argument which I removed. Should I leave a porting note, and if so what kind?

Jireh Loreaux (Mar 12 2023 at 21:23):

What do you mean by "removed"? Just _? No need for a note.

Jeremy Tan (Mar 12 2023 at 21:23):

https://github.com/leanprover-community/mathlib4/pull/2831/commits/8f5c251a972496db9afe14bc4c3565d5437b48c9 I mean this

Jeremy Tan (Mar 12 2023 at 21:24):

Not just _ replacement; an entire argument to a function was marked by the linter as unused

Jireh Loreaux (Mar 12 2023 at 21:26):

It might be there on purpose. Adam will know. I would suggest leaving it (otherwise you definitely need a porting note as well as an #align with an x.

Adam Topaz (Mar 12 2023 at 21:30):

Sorry, I’m on mobile now and can’t really check such things. Who wrote the original file? Maybe they will know immediately

Jireh Loreaux (Mar 12 2023 at 21:31):

@Johan Commelin see above

Jeremy Tan (Mar 13 2023 at 04:14):

!4#2832 can someone help with the remaining issues over here?

Joël Riou (Mar 13 2023 at 14:36):

Jeremy Tan said:

!4#2832 can someone help with the remaining issues over here?

In principle, I have fixed the issues https://github.com/leanprover-community/mathlib4/pull/2832/commits/7cfe34201d5116ff4244c58ae8870bcc10689ad8

Last updated: Dec 20 2023 at 11:08 UTC