digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
306 stars 40 forks source link

fix tutorial instructions #94

Closed tlyu closed 2 years ago

tlyu commented 2 years ago

The MMB file is the argument to mm0-c, and the MM0 file is the redirected input. (The basename is also different, because it came from an earlier tutorial step.) mm0-c won't parse an MM1 file.