Constants used in the MMB specification.
| DATA_8 | DATA_8 = 0x40, used as a command mask for an 8 bit data field
|
| DATA_16 | DATA_16 = 0x80, used as a command mask for a 16 bit data field
|
| DATA_32 | DATA_32 = 0xC0, used as a command mask for a 32 bit data field
|
| DATA_MASK | DATA_MASK = 0xC0, selects one of DATA_8, DATA_16, or DATA_32 for data size
|
| INDEX_HYP_NAME | "HypN" is the magic number for the hypothesis name table.
|
| INDEX_NAME | "Name" is the magic number for the name table.
|
| INDEX_VAR_NAME | "VarN" is the magic number for the variable name table.
|
| MM0B_MAGIC | MM0B_MAGIC = "MM0B": Magic number signalling the MM0B format is in use.
|
| MM0B_VERSION | MM0B_VERSION = 1, maximum supported MMB version
|
| PROOF_CONG | PROOF_CONG = 0x1A: See ProofCmd.
|
| PROOF_CONV | PROOF_CONV = 0x17: See ProofCmd.
|
| PROOF_CONV_CUT | PROOF_CONV_CUT = 0x1C: See ProofCmd.
|
| PROOF_CONV_SAVE | PROOF_CONV_SAVE = 0x1E: See ProofCmd.
|
| PROOF_DUMMY | PROOF_DUMMY = 0x13: See ProofCmd.
|
| PROOF_HYP | PROOF_HYP = 0x16: See ProofCmd.
|
| PROOF_REF | PROOF_REF = 0x12: See ProofCmd.
|
| PROOF_REFL | PROOF_REFL = 0x18: See ProofCmd.
|
| PROOF_SAVE | PROOF_SAVE = 0x1F: See ProofCmd.
|
| PROOF_SORRY | PROOF_SORRY = 0x20: See ProofCmd.
|
| PROOF_SYMM | PROOF_SYMM = 0x19: See ProofCmd.
|
| PROOF_TERM | PROOF_TERM = 0x10: See ProofCmd.
|
| PROOF_TERM_SAVE | PROOF_TERM_SAVE = 0x11: See ProofCmd.
|
| PROOF_THM | PROOF_THM = 0x14: See ProofCmd.
|
| PROOF_THM_SAVE | PROOF_THM_SAVE = 0x15: See ProofCmd.
|
| PROOF_UNFOLD | PROOF_UNFOLD = 0x1B: See ProofCmd.
|
| STMT_AXIOM | STMT_AXIOM = 0x02, starts an axiom declaration
|
| STMT_DEF | STMT_DEF = 0x05, starts a def declaration. (This is the same as
STMT_TERM because the actual indication of whether this is a
def is in the term header)
|
| STMT_LOCAL | STMT_LOCAL = 0x08, starts a local declaration
(a bit mask to be combined with STMT_THM or STMT_DEF)
|
| STMT_LOCAL_DEF | STMT_LOCAL_DEF = 0x0D
|
| STMT_LOCAL_THM | STMT_LOCAL_THM = 0x0E
|
| STMT_SORT | STMT_SORT = 0x04, starts a sort declaration
|
| STMT_TERM | STMT_TERM = 0x05, starts a term declaration
|
| STMT_THM | STMT_THM = 0x06, starts a theorem declaration
|
| UNIFY_DUMMY | UNIFY_DUMMY = 0x33: See UnifyCmd.
|
| UNIFY_HYP | UNIFY_HYP = 0x36: See UnifyCmd.
|
| UNIFY_REF | UNIFY_REF = 0x32: See UnifyCmd.
|
| UNIFY_TERM | UNIFY_TERM = 0x30: See UnifyCmd.
|
| UNIFY_TERM_SAVE | UNIFY_TERM_SAVE = 0x31: See UnifyCmd.
|