search

digama0 / mm0

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

Proof stream opcode "Hyp" pushes to heap instead of stack. #3

Closed IvoWingelaar closed 4 years ago

IvoWingelaar commented 4 years ago

In mm0-c, the comments near the execution of CMD_PROOF_HYP claims it pushes |- e to the main stack (as specified in the paper), but the code pushes it to the main heap instead.

digama0 commented 4 years ago

The code's behavior is the correct one. (We don't usually have any guarantee that the hypotheses will be used, or used in the right order, so it is more convenient to have them in the heap instead so we can reference them 0 or more times.) I will update the paper.

digama0 commented 4 years ago

The comment to mm0-c/verifier.c for CMD_PROOF_HYP was also in error; fixed in 0c556a2.