ListM

Stream: std4

[Scott Morrison]

I would like to try upstreaming ListM from mathlib4 to std4, as a step towards upstreaming exact? (the tactic formerly known as library_search).

The PR backlog notwithstanding, @Mario Carneiro, might you be able to tell me whether you'd prefer that I

• open a PR with the whole file
• open a minimal PR with as little as possible
• neither, and refactor exact? to avoid using ListM in the first place. (It is used there to separate the "travering the library" logic from the "deciding we're done" logic.)

[Mario Carneiro]

the file seems like a good PR unit

[Scott Morrison]

https://github.com/leanprover/std4/pull/165

(the mathlib4 file had some Mathlib imports, but ... they are apparently unnecessary!)