Skip to main content

oxilean_codegen/coq_backend/
coqclassdef_traits.rs

1//! # CoqClassDef - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqClassDef`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqClassDef;
12use std::fmt;
13
14impl std::fmt::Display for CoqClassDef {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        let params: Vec<String> = self
17            .params
18            .iter()
19            .map(|(n, t)| format!("({} : {})", n, t))
20            .collect();
21        write!(f, "Class {}", self.name)?;
22        if !params.is_empty() {
23            write!(f, " {}", params.join(" "))?;
24        }
25        writeln!(f, " := {{")?;
26        for (mname, mtype) in &self.methods {
27            writeln!(f, "  {} : {};", mname, mtype)?;
28        }
29        write!(f, "}}.")
30    }
31}