public class SetMMConstants
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SetMMConstants.NotSetMMContext |
Modifier and Type | Field and Description |
---|---|
Axiom |
CAB |
Cnst |
CLASS |
Axiom |
CV |
Cnst |
DED |
static ErrorCode |
ERRMSG_AX_HAS_DV |
static ErrorCode |
ERRMSG_AX_NOT_EXISTS |
static ErrorCode |
ERRMSG_AX_WRONG_TYPE |
static ErrorCode |
ERRMSG_NEW_AXIOM |
static ErrorCode |
ERRMSG_REUSE_SET_IN_DEFN |
static ErrorCode |
ERRMSG_STMT_NOT_AX |
static ErrorCode |
ERRMSG_SYM_NOT_EXISTS |
static ErrorCode |
ERRMSG_SYM_NOT_TYPECODE |
static ErrorCode |
ERRMSG_THM_IN_SYNTAX |
Cnst |
SET |
Axiom |
WA |
Axiom |
WAL |
Axiom |
WB |
Axiom |
WCEL |
Axiom |
WCEQ |
Axiom |
WEX |
Cnst |
WFF |
Axiom |
WI |
Axiom |
WN |
Axiom |
WO |
Axiom |
WTRU |
Constructor and Description |
---|
SetMMConstants(ProofAsst pa)
Create an instance of
SetMMConstants . |
public static final ErrorCode ERRMSG_SYM_NOT_EXISTS
public static final ErrorCode ERRMSG_SYM_NOT_TYPECODE
public static final ErrorCode ERRMSG_AX_NOT_EXISTS
public static final ErrorCode ERRMSG_STMT_NOT_AX
public static final ErrorCode ERRMSG_AX_WRONG_TYPE
public static final ErrorCode ERRMSG_AX_HAS_DV
public static final ErrorCode ERRMSG_NEW_AXIOM
public static final ErrorCode ERRMSG_THM_IN_SYNTAX
public static final ErrorCode ERRMSG_REUSE_SET_IN_DEFN
public final Cnst SET
public final Cnst CLASS
public final Cnst WFF
public final Cnst DED
public final Axiom WN
public final Axiom WI
public final Axiom WB
public final Axiom WA
public final Axiom WO
public final Axiom WTRU
public final Axiom WAL
public final Axiom WEX
public final Axiom CV
public final Axiom WCEQ
public final Axiom WCEL
public final Axiom CAB
public SetMMConstants(ProofAsst pa) throws SetMMException
SetMMConstants
. This function checks that
all typecodes and syntax axioms it provides exist and have the right
type.pa
- SetMMException