oxilean_codegen/lean4_backend/
lean4pattern_traits.rs

1//! # Lean4Pattern - Trait Implementations
2//!
3//! This module contains trait implementations for `Lean4Pattern`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::functions::*;
12use super::types::Lean4Pattern;
13use std::fmt;
14
15impl fmt::Display for Lean4Pattern {
16    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
17        match self {
18            Lean4Pattern::Wildcard => write!(f, "_"),
19            Lean4Pattern::Var(name) => write!(f, "{}", name),
20            Lean4Pattern::Ctor(name, args) => {
21                write!(f, "{}", name)?;
22                for arg in args {
23                    write!(f, " {}", paren_pattern(arg))?;
24                }
25                Ok(())
26            }
27            Lean4Pattern::Tuple(pats) => {
28                write!(f, "(")?;
29                for (i, p) in pats.iter().enumerate() {
30                    if i > 0 {
31                        write!(f, ", ")?;
32                    }
33                    write!(f, "{}", p)?;
34                }
35                write!(f, ")")
36            }
37            Lean4Pattern::Lit(s) => write!(f, "{}", s),
38            Lean4Pattern::Or(a, b) => write!(f, "{} | {}", a, b),
39            Lean4Pattern::Anonymous(pats) => {
40                write!(f, "⟨")?;
41                for (i, p) in pats.iter().enumerate() {
42                    if i > 0 {
43                        write!(f, ", ")?;
44                    }
45                    write!(f, "{}", p)?;
46                }
47                write!(f, "⟩")
48            }
49        }
50    }
51}
oxilean_codegen/lean4_backend/lean4pattern_traits.rs

oxilean_codegen/lean4_backend/
lean4pattern_traits.rs
