trivial-kernel 0.9.0

A Metamath Zero kernel for Trivial
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
pub enum Kind {
    InvalidHeapIndex,
    InvalidProofIndex,
    InvalidTheorem,
    InvalidStoreIndex,
    InvalidStoreType,
    InvalidTerm,
    InvalidStoreExpr,
    InvalidSort,
    InvalidBinderIndices,
    InvalidUnifyCommandIndex,
    InvalidStackType,
    IncompatibleTypes,
    DependencyOverflow,
    UnifyStackUnderflow,
    CantSaveConvertabilityObligation,
    UnifyRefFailure,
    UnifyTermFailure,
    ProofStackUnderflow,
    SortNotProvable,
    SortIsStrict,
    SortIsPure,
    StackHasMoreThanOne,
    UnaccountedDependencies,
    BadReturnType,
    TypeError,
    TooManyBoundVariables,
    HypStackUnderflow,
    DummyCommandInTheorem,
    CongUnifyError,
    BindDep,
    DisjointVariableViolation,
    UnknownCommand,
    UnfinishedHypStack,
    UnfinishedUnifyStack,
    HypInDefStatement,
    InvalidOpcodeInDef,
    Impossible,
    TheoremOutOfRange,
    TermOutOfRange,
    SortOutOfRange,
    StreamExhausted,
    MissingProofStream,
}

/// A typedef for the result from a kernel method.
pub type KResult<O = ()> = Result<O, Kind>;