oxilean_kernel/inductive/
inductiveerror_traits.rs1use super::types::InductiveError;
12
13impl std::fmt::Display for InductiveError {
14 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
15 match self {
16 InductiveError::AlreadyDefined(n) => {
17 write!(f, "type '{}' is already defined", n)
18 }
19 InductiveError::UndefinedType(n) => write!(f, "undefined type '{}'", n),
20 InductiveError::InvalidConstructorType(n) => {
21 write!(f, "invalid constructor type for '{}'", n)
22 }
23 InductiveError::UniverseTooSmall(s) => write!(f, "universe too small: {}", s),
24 InductiveError::NonStrictlyPositive(n) => {
25 write!(f, "non-strictly-positive occurrence of '{}'", n)
26 }
27 InductiveError::Other(s) => write!(f, "inductive error: {}", s),
28 }
29 }
30}