You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
$$ target/release/metamath-knife --text A '$[ B $] $[ C $]' \
--text B '$[ C $] $c X $.' --text C '$c X $.'
C:3-4:Error:This symbol is already active in this scope
B:11-12:Note:Symbol was previously declared here
A starts by including B which starts by including C, so C's version of X should be the logically first one, but metamath-knife gets confused during readahead and decides that the "real" include of C is the one in A, messing up the order. The included check in read_and_parse is misplaced, not sure right now where it belongs.
The text was updated successfully, but these errors were encountered:
From
SMM3
issue #22A
starts by includingB
which starts by includingC
, soC
's version ofX
should be the logically first one, but metamath-knife gets confused during readahead and decides that the "real" include ofC
is the one inA
, messing up the order. Theincluded
check inread_and_parse
is misplaced, not sure right now where it belongs.The text was updated successfully, but these errors were encountered: