Zulip Chat Archive

Stream: general

Topic: partial finset.filter?

Kenny Lau (Sep 07 2018 at 07:00):


finset.filter : Π {α : Type u_1} (p : α  Prop) [_inst_3 : decidable_pred p], finset α  finset α

I wonder if there's a similar function, but instead of defining p everywhere, just define it on the input finset?

Last updated: Dec 20 2023 at 11:08 UTC