List.Chain' that fixes both ends

Stream: Is there code for X?

[Paige Thomas]

Does this already exist in Mathlib somewhere?

inductive Walk {α : Type} (R : α -> α -> Prop) : α -> List α -> α -> Prop
| one (a : α) : Walk R a [] a
| cons (a b c : α) (l : List α) : R a b -> Walk R b l c -> Walk R a (b :: l) c

[Floris van Doorn]

docs#SimpleGraph.Walk if your R is symmetric and irreflexive.

[Floris van Doorn]

docs#SimpleGraph.Walk.support gives the list.

[Paige Thomas]

Hmm. I see. Thank you.

[Paige Thomas]

Floris van Doorn said:

docs#SimpleGraph.Walk if your R is symmetric and irreflexive.

I'm not sure it is.

[Yury G. Kudryashov]

You can use List.Chain' R (a :: l ++ [b])

[Paige Thomas]

That makes sense. Thank you.