Method fmt

lean-agentic/src/level.rs:68–77

(&self, f: &mut fmt::Formatter<'_>)

impl fmt::Display for Level {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Level::Zero => write!(f, "0"),
            Level::Const(n) => write!(f, "{}", n),
            Level::Param(n) => write!(f, "u{}", n),
            Level::Succ(id) => write!(f, "(succ {})", id.0),
            Level::Max(a, b) => write!(f, "(max {} {})", a.0, b.0),
            Level::IMax(a, b) => write!(f, "(imax {} {})", a.0, b.0),
        }
    }
}

/// Arena for interning universe levels