Skip to main content

oxilean_kernel/level/
level_traits.rs

1//! # Level - Trait Implementations
2//!
3//! This module contains trait implementations for `Level`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::Level;
12use std::fmt;
13
14impl fmt::Display for Level {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        match self {
17            Level::Zero => write!(f, "0"),
18            Level::Succ(l) => {
19                if let Some(n) = self.to_nat() {
20                    write!(f, "{}", n)
21                } else {
22                    write!(f, "({} + 1)", l)
23                }
24            }
25            Level::Max(l1, l2) => write!(f, "max({}, {})", l1, l2),
26            Level::IMax(l1, l2) => write!(f, "imax({}, {})", l1, l2),
27            Level::Param(n) => write!(f, "{}", n),
28            Level::MVar(id) => write!(f, "?u_{}", id.0),
29        }
30    }
31}