$ target/release/smetamath --verify test.mm
test.mm:1:8:Warning:Proof is incomplete
Note that there are seven printable characters on the first line, so 1:8 is likely the \r before the newline. This is due to the span calculation for the statement, which includes the leading whitespace before the theorem, up through the end of the $p statement (which is not being printed in the error message). This span should be shrunk to begin at the a label, so that it reads 2:1 instead.
Given the input file
test.mm
:Output:
Note that there are seven printable characters on the first line, so
1:8
is likely the\r
before the newline. This is due to the span calculation for the statement, which includes the leading whitespace before the theorem, up through the end of the$p
statement (which is not being printed in the error message). This span should be shrunk to begin at thea
label, so that it reads2:1
instead.