Open
Description
File that generates the bug:
ax1 $a A $. th1 $p A $= ax1 $.
Metamath-exe interface:
Metamath - Version 0.199.pre 29-Jan-2022 Type HELP for help, EXIT to exit. MM> set scroll continuous Continuous scrolling is now in effect. MM> read issue169.mm /verify Reading source file "issue169.mm"... 32 bytes 32 bytes were read into the source buffer. The source has 2 statements; 1 are $a and 1 are $p. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ This math symbol was not declared (with a "$c" or "$v" statement). ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ The first symbol must be a constant in a "$a" statement. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. ^ This variable does not occur in any active "$e" or "$f" hypothesis. All variables in "$a" and "$p" statements must appear in at least one such hypothesis. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. ?Error on line 1 of file "issue169.mm" at statement 1, label "ax1", type "$a": ax1 $a A $. The variable "A" does not appear in an active "$f" statement. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ This math symbol was not declared (with a "$c" or "$v" statement). ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ The first symbol must be a constant in a "$p" statement. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. ^ This variable does not occur in any active "$e" or "$f" hypothesis. All variables in "$a" and "$p" statements must appear in at least one such hypothesis. ?Error on line 3 of file "issue169.mm" at statement 2, label "th1", type "$p": th1 $p A $= ax1 $. The variable "A" does not appear in an active "$f" statement. 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% ..................................................?BUG CHECK: *** DETECTED BUG 2103 To get technical support, please open an issue (https://github.com/metamath/metamath-exe/issues) with the detailed command sequence or a command file that reproduces this bug, along with the source file that was used. See HELP OPEN LOG for help on recording a session. See HELP SUBMIT for help on command files. Search for "bug(2103)" in the m*.c source code to find its origin. If earlier errors were reported, try fixing them first, because they may occasionally lead to false bug detection Press S to step to next bug, I to ignore further bugs, or A to abort program: S Warning!!! A bug was detected, but you are continuing anyway. The program may be corrupted, so you are proceeding at your own risk. 8 errors were found. MM>
Without the /VERIFY
option the bug does not occur (the verify proof *
command triggers the bug as well).
Metadata
Metadata
Assignees
Labels
No labels