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: Mar 28 2024 at 12:29 UTC