oxilean_codegen/lean4_backend/
lean4dostmt_traits.rs

1//! # Lean4DoStmt - Trait Implementations
2//!
3//! This module contains trait implementations for `Lean4DoStmt`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::Lean4DoStmt;
12use std::fmt;
13
14impl fmt::Display for Lean4DoStmt {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        match self {
17            Lean4DoStmt::Bind(name, ty, expr) => {
18                if let Some(t) = ty {
19                    write!(f, "let ({} : {}) ← {}", name, t, expr)
20                } else {
21                    write!(f, "let {} ← {}", name, expr)
22                }
23            }
24            Lean4DoStmt::LetBind(name, ty, expr) => {
25                if let Some(t) = ty {
26                    write!(f, "let {} : {} := {}", name, t, expr)
27                } else {
28                    write!(f, "let {} := {}", name, expr)
29                }
30            }
31            Lean4DoStmt::Expr(e) => write!(f, "{}", e),
32            Lean4DoStmt::Return(e) => write!(f, "return {}", e),
33            Lean4DoStmt::Pure(e) => write!(f, "pure {}", e),
34            Lean4DoStmt::If(cond, then_stmts, else_stmts) => {
35                write!(f, "if {} then", cond)?;
36                for s in then_stmts {
37                    write!(f, "\n    {}", s)?;
38                }
39                if !else_stmts.is_empty() {
40                    write!(f, "\n  else")?;
41                    for s in else_stmts {
42                        write!(f, "\n    {}", s)?;
43                    }
44                }
45                Ok(())
46            }
47        }
48    }
49}
oxilean_codegen/lean4_backend/lean4dostmt_traits.rs

oxilean_codegen/lean4_backend/
lean4dostmt_traits.rs
