list.filter bool

Stream: general

[Jiatong Yang]

How can I use list.filter with (α -> bool) (lean asks me to use (α -> Prop) with a decidable instance)? Btw, I think my solution is too long and I must have missed some useful api.

import data.list
def l := [[0,1,2],[3,4,5],[7,8],[1,4],[2,5,8],[3,6,8],[1,6,7]]

def is_same (l : list ℕ) := l.all (λ x, x = l.head)

def ok (p : list ℕ) := is_same $ l.map (list.sum ∘ list.map (flip option.get_or_else 0 ∘ p.nth))

#eval [1,2,3,4,5,6,7,8,9].permutations.filter ok

[Yaël Dillies]

Ìf l : list α, f : α → bool, then l.filter (λ a, f a) should work as Lean will the coercion from bool to Prop.

[Jiatong Yang]

It works! Thank you!

[Jiatong Yang]

I found that flip option.get_or_else 0 ∘ p.nth can be replaced by p.inth.
There's another question: how to run the program? (I couldn't eval it as I got a "timeout")

[Matt Diamond]

there's also list.nthd if you want to specify the default yourself instead of relying on the type's default