Decidable List equal empty.

Stream: Is there code for X?

[Wrenna Robson]

Do we not have this?

import Mathlib

namespace List

instance {l : List α} : Decidable (l = []) := decidable_of_iff _ List.length_eq_zero

end List

[Wrenna Robson]

It seems like an obvious thing to have but I can't find it!

[Yakov Pechersky]

Unfortunately this likely clashes with other Decidable when DecidableEq

[Yakov Pechersky]

In what situation do you need this? It's probably fine to have Decidable (l = []) as a TC assumption. Are you trying to avoid writing this instance argument?

[Eric Wieser]

I assume the motivation here is that DecidableEq α does not hold; can you avoid this by using if let [] := l then _ else _ instead of if l = [] then _ else _?

[Wrenna Robson]

I actually found a way round it for now

[Violeta Hernández]

Seems weird to need this, surely you can just match on l instead?

[Kyle Miller]

docs#List.isEmpty is one of the main ways to avoid this. You can write if l.isEmpty then _ else _.

[Kyle Miller]

The expression version of Eric's suggestion is if l matches [] then _ else _. It can be nicer since it doesn't need to be the top-level of the if condition, but l.isEmpty wins out if you're counting characters.

[Wrenna Robson]

Aye. I basically think sometimes we use "l = []" in theorems when we should use that

[Eric Wieser]

One is a bool and the other a Prop, so we should generally use the one that doesn't cause a superfluous coercion