Number of statements

[amelieled]

I don't understand how the official C implementation of Metamath computes the number of statements.

For instance, I get

Reading source file "demo0.mm"... 2251 bytes
2251 bytes were read into the source buffer.
The source has 19 statements; 7 are $a and 1 are $p.

whereas there are 1 $c, 1 $v, 5 $f, 0 $d, 2 $e, 7 $a and 1 $p, i.e. 17 declarations.

[digama0]

I would expect from those numbers that $c, $v, $d are not counted as statements. What the others have in common is that they have label names.

Oh wait, the number is too low by 2. Are you counting ${ and $} as well?

[amelieled]

There are 1 ${ and 1 $}.

[digama0]

I think the way metamath parses statements would count those as statements as well.

[amelieled]

But it is very strange since if there is one ${, then there is one $}.

[amelieled]

For the file big-unifier.mm:
29 statements = 1 $c + 1 $v + 17 $f + 2 $e + 4 $a + 2 $p + 1 ${ + 1 $}.

[digama0]

I think the number should be taken with a grain of salt. As I understand it this is just reporting the size of the underlying statement array without doing any particular filtering, and so anything which is represented in there gets counted. In metamath-knife there are also "statements" for $t and $j comments.

[amelieled]

Ok so "statement" for the official C implementation of Metamath is the number of keywords (except $(, $), $[, $], $t and $j), and for metamath-knife, is the number of keywords (except $(, $), $[ and $]), or something like that.

[digama0]

Include directives $[ foo.mm $] might count as one statement in metamath-exe, I'm not sure. (They are a bit weird since they get replaced by their contents so they may count as the number of statements in the target file, or maybe the number of statement in the target + 1.)