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)]
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,
}
pub type KResult<O = ()> = Result<O, Kind>;