Adrien Champion

> `List.modifyHead` should not be `simp`. I think most of those are mistakes, that kind of thing used to work in lean 3 but in lean 4 it unfolds directly...

Done, I made `modifyHead_modifyHead` just be `simp` instead of `simp 1100` since the linter authorized me

I'm fine with splitting this PR if you let me know what does (not) deserve to be merged immediately. Regarding `length_eq_three` I don't have an argument for it, it's only...

> Is there a matching Mathlib PR? It would be nice to be able to verify that Mathlib can be updated cleanly. > > (Maybe you know this already, but...

On that note, this PR is awaiting reviews, not author, could you change the label back @semorrison please?

Is there something blocking this PR on my end? Is it maybe the mathlib PR, should I open one to move on on this one?

I think so, thank you for pointing it out

By the way, a way around that problem would be for you to support the `echo` command. That way tools could send a `(echo "success")` after issuing a command. Maybe...

I see, thank you for your answer and good luck :)

Thank you for your bug report :) Sorry it took so long to get back to you. As you might have noticed the repo is flagged for security vulnerabilities, which...