cycle.next and list.next

Stream: Is there code for X?

[Sky Wilshaw]

Is there code relating cycle.next and list.next ∘ cycle.coe?

[Patrick Johnson]

What do you mean by list.next ∘ cycle.coe? Function cycle.next is defined in terms of list.next over quotients, so they are definitionally equal:

import data.list.cycle

example {α : Type*} [decidable_eq α] {l : list α} {x : α} {h₁ h₂} :
  l.next x h₁ = (l : cycle α).next h₂ x h₁ :=
by refl

[Sky Wilshaw]

Oh right, I didn't realise that. I thought I'd have to do some weird conversions with quotients manually, but this helps a lot.