oxilean_codegen/coq_backend/
coqtacticext_traits.rs

1//! # CoqTacticExt - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqTacticExt`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqTacticExt;
12use std::fmt;
13
14impl std::fmt::Display for CoqTacticExt {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        match self {
17            CoqTacticExt::Intro(hs) => write!(f, "intros {}", hs.join(" ")),
18            CoqTacticExt::Apply(l) => write!(f, "apply {}", l),
19            CoqTacticExt::Exact(e) => write!(f, "exact ({})", e),
20            CoqTacticExt::Rewrite(bwd, l) => {
21                if *bwd {
22                    write!(f, "rewrite <- {}", l)
23                } else {
24                    write!(f, "rewrite {}", l)
25                }
26            }
27            CoqTacticExt::Simpl => write!(f, "simpl"),
28            CoqTacticExt::Ring => write!(f, "ring"),
29            CoqTacticExt::Omega => write!(f, "omega"),
30            CoqTacticExt::Lia => write!(f, "lia"),
31            CoqTacticExt::Lra => write!(f, "lra"),
32            CoqTacticExt::Auto => write!(f, "auto"),
33            CoqTacticExt::EAuto => write!(f, "eauto"),
34            CoqTacticExt::Tauto => write!(f, "tauto"),
35            CoqTacticExt::Constructor => write!(f, "constructor"),
36            CoqTacticExt::Split => write!(f, "split"),
37            CoqTacticExt::Left => write!(f, "left"),
38            CoqTacticExt::Right => write!(f, "right"),
39            CoqTacticExt::Exists(w) => write!(f, "exists {}", w),
40            CoqTacticExt::Induction(h) => write!(f, "induction {}", h),
41            CoqTacticExt::Destruct(h) => write!(f, "destruct {}", h),
42            CoqTacticExt::Inversion(h) => write!(f, "inversion {}", h),
43            CoqTacticExt::Reflexivity => write!(f, "reflexivity"),
44            CoqTacticExt::Symmetry => write!(f, "symmetry"),
45            CoqTacticExt::Transitivity(t) => write!(f, "transitivity ({})", t),
46            CoqTacticExt::Unfold(ls) => write!(f, "unfold {}", ls.join(", ")),
47            CoqTacticExt::Fold(ls) => write!(f, "fold {}", ls.join(", ")),
48            CoqTacticExt::Assumption => write!(f, "assumption"),
49            CoqTacticExt::Contradiction => write!(f, "contradiction"),
50            CoqTacticExt::Exfalso => write!(f, "exfalso"),
51            CoqTacticExt::Clear(hs) => write!(f, "clear {}", hs.join(" ")),
52            CoqTacticExt::Rename(a, b) => write!(f, "rename {} into {}", a, b),
53            CoqTacticExt::Trivial => write!(f, "trivial"),
54            CoqTacticExt::Discriminate => write!(f, "discriminate"),
55            CoqTacticExt::Injection(h) => write!(f, "injection {}", h),
56            CoqTacticExt::FApply(l) => write!(f, "eapply {}", l),
57            CoqTacticExt::Subst(h) => {
58                if let Some(h) = h {
59                    write!(f, "subst {}", h)
60                } else {
61                    write!(f, "subst")
62                }
63            }
64            CoqTacticExt::Custom(s) => write!(f, "{}", s),
65        }
66    }
67}
oxilean_codegen/coq_backend/coqtacticext_traits.rs

oxilean_codegen/coq_backend/
coqtacticext_traits.rs
