Module cmd 

Constants used in the MMB specification.

Constants

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.