oxilean_codegen/idris_backend/
idristactic_traits.rs

1//! # IdrisTactic - Trait Implementations
2//!
3//! This module contains trait implementations for `IdrisTactic`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::IdrisTactic;
12use std::fmt;
13
14impl fmt::Display for IdrisTactic {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        match self {
17            IdrisTactic::Intro(x) => write!(f, "intro {}", x),
18            IdrisTactic::Intros => write!(f, "intros"),
19            IdrisTactic::Exact(e) => write!(f, "exact {}", e),
20            IdrisTactic::Refl => write!(f, "refl"),
21            IdrisTactic::Trivial => write!(f, "trivial"),
22            IdrisTactic::Decide => write!(f, "decide"),
23            IdrisTactic::Rewrite(h) => write!(f, "rewrite {}", h),
24            IdrisTactic::RewriteBack(h) => write!(f, "rewrite <- {}", h),
25            IdrisTactic::Apply(func) => write!(f, "apply {}", func),
26            IdrisTactic::Cases(x) => write!(f, "cases {}", x),
27            IdrisTactic::Induction(x) => write!(f, "induction {}", x),
28            IdrisTactic::Search => write!(f, "search"),
29            IdrisTactic::Auto => write!(f, "auto"),
30            IdrisTactic::With(e) => write!(f, "with {}", e),
31            IdrisTactic::Let(x, e) => write!(f, "let {} = {}", x, e),
32            IdrisTactic::Have(x, t) => write!(f, "have {} : {}", x, t),
33            IdrisTactic::Focus(n) => write!(f, "focus {}", n),
34            IdrisTactic::Claim(n, t) => write!(f, "claim {} : {}", n, t),
35            IdrisTactic::Unfold(n) => write!(f, "unfold {}", n),
36            IdrisTactic::Compute => write!(f, "compute"),
37            IdrisTactic::Normals => write!(f, "normals"),
38            IdrisTactic::Fail(msg) => write!(f, "fail \"{}\"", msg),
39            IdrisTactic::Seq(ts) => {
40                for (i, t) in ts.iter().enumerate() {
41                    if i > 0 {
42                        write!(f, "; ")?;
43                    }
44                    write!(f, "{}", t)?;
45                }
46                Ok(())
47            }
48        }
49    }
50}
oxilean_codegen/idris_backend/idristactic_traits.rs

oxilean_codegen/idris_backend/
idristactic_traits.rs
