Skip to main content

oxilean_codegen/coq_backend/
coqletdef_traits.rs

1//! # CoqLetDef - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqLetDef`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqLetDef;
12use std::fmt;
13
14impl std::fmt::Display for CoqLetDef {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        let kw = if self.is_opaque {
17            "Opaque"
18        } else {
19            "Transparent"
20        };
21        write!(f, "Definition {}", self.name)?;
22        for (pn, pt) in &self.params {
23            if let Some(t) = pt {
24                write!(f, " ({} : {})", pn, t)?;
25            } else {
26                write!(f, " {}", pn)?;
27            }
28        }
29        if let Some(rt) = &self.return_type {
30            write!(f, " : {}", rt)?;
31        }
32        write!(f, " := {}.", self.body)?;
33        if self.is_opaque {
34            write!(f, "\n{} {}.", kw, self.name)?;
35        }
36        Ok(())
37    }
38}