Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Q.PAT_X_ASSUM (akaqpat_x_assum) returns bad error messages because its implementation can't distinguish between an expected failure (the pattern not matching an unrelated assumption) and an unexpected failure (the continuation failing). Sometimes this is inevitable because there may be multiple parses for the pattern, but if there's only one, the error could be better. (Incidentally, the behaviour probably shouldn't be to try to find the first assumption that both matches the pattern and has the continuation succeed.)
Q.PAT_X_ASSUM(akaqpat_x_assum) returns bad error messages because its implementation can't distinguish between an expected failure (the pattern not matching an unrelated assumption) and an unexpected failure (the continuation failing). Sometimes this is inevitable because there may be multiple parses for the pattern, but if there's only one, the error could be better. (Incidentally, the behaviour probably shouldn't be to try to find the first assumption that both matches the pattern and has the continuation succeed.)Prompted by some discussion on Discord .