oxilean_codegen/coq_backend/
coqinductivedef_traits.rs

1//! # CoqInductiveDef - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqInductiveDef`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqInductiveDef;
12use std::fmt;
13
14impl std::fmt::Display for CoqInductiveDef {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        let kw = if self.is_coinductive {
17            "CoInductive"
18        } else {
19            "Inductive"
20        };
21        let params: Vec<String> = self
22            .params
23            .iter()
24            .map(|(n, t)| format!("({} : {})", n, t))
25            .collect();
26        let indices: Vec<String> = self
27            .indices
28            .iter()
29            .map(|(n, t)| format!("({} : {})", n, t))
30            .collect();
31        write!(f, "{} {}", kw, self.name)?;
32        if !params.is_empty() {
33            write!(f, " {}", params.join(" "))?;
34        }
35        if !indices.is_empty() {
36            write!(f, " : {} -> {}", indices.join(" -> "), self.universe)?;
37        } else {
38            write!(f, " : {}", self.universe)?;
39        }
40        writeln!(f, " :=")?;
41        for (cname, cargs, _ret) in &self.constructors {
42            let args: Vec<String> = cargs
43                .iter()
44                .map(|(n, t)| format!("({} : {})", n, t))
45                .collect();
46            if args.is_empty() {
47                writeln!(f, "| {} : {}", cname, self.name)?;
48            } else {
49                writeln!(f, "| {} : {} -> {}", cname, args.join(" -> "), self.name)?;
50            }
51        }
52        write!(f, ".")
53    }
54}
oxilean_codegen/coq_backend/coqinductivedef_traits.rs

oxilean_codegen/coq_backend/
coqinductivedef_traits.rs
