Stream: Beginner Questions

Topic: "Enter MATCH" output

view this post on Zulip waynee95 (Aug 04 2022 at 19:29):

What does Enter MATCH mean, when you get that in the output window?

view this post on Zulip Lawrence Paulson (Aug 14 2022 at 17:30):

It's a sign that higher-order unification is probably working too hard. It's pretty rare to get a proof once you see this, so try another approach.

Last updated: Jun 06 2026 at 17:17 UTC