chore: add warning comments about `findM?`

[kim-em]

[kim-em]

Pinging @arthur-adjedj, just FYI.

[arthur-adjedj]

Thank you for the ping, I didn't take that into consideration when writing that function. occursOrInType could be rewritten with the non-monadic find by passing the LocalContext to the function and fetching the type of fvars there. Doing so might be the better option compared to keeping findM in the codebase.

[kim-em]

Thank you for the ping, I didn't take that into consideration when writing that function. FYI, occursOrInType could be rewritten with the non-monadic find by passing the LocalContext to the function and fetching the type of fvars there. Doing so might be the better option compared to keeping findM in the codebase.

If you'd be interested in doing that, I'd love to merge it. :-) findM? seems like a scary footgun to leave around.

[arthur-adjedj]

Right. I'm not available to work on this now, but will make an according PR to fix occursOrInType and to remove the monadic find by the end of the day.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ca6437df717b550cbea3e110f3093c1250d5c5be --onto fe7b96d8a0cf85e1ea81791ac9d673f84c9e866d. (2024-05-10 07:09:17)

[kim-em]

Obsolete given #4125.