Skip to main content

oxilean_codegen/coq_backend/
coqltacdef_traits.rs

1//! # CoqLtacDef - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqLtacDef`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqLtacDef;
12use std::fmt;
13
14impl std::fmt::Display for CoqLtacDef {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        let rec = if self.is_recursive { " Recursive" } else { "" };
17        if self.params.is_empty() {
18            write!(f, "Ltac{} {} := {}.", rec, self.name, self.body)
19        } else {
20            write!(
21                f,
22                "Ltac{} {} {} := {}.",
23                rec,
24                self.name,
25                self.params.join(" "),
26                self.body
27            )
28        }
29    }
30}