Skip to main content

oxilean_codegen/coq_backend/
coqinstancedef_traits.rs

1//! # CoqInstanceDef - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqInstanceDef`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqInstanceDef;
12use std::fmt;
13
14impl std::fmt::Display for CoqInstanceDef {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        let nm = self.name.as_deref().unwrap_or("_");
17        let args = self.args.join(" ");
18        write!(
19            f,
20            "#[global] Instance {} : {} {} :=\n{{",
21            nm, self.class, args
22        )?;
23        for (mn, mb) in &self.methods {
24            write!(f, "\n  {} := {};", mn, mb)?;
25        }
26        write!(f, "\n}}.")
27    }
28}