oxilean_codegen/coq_backend/
coqextraction_traits.rs

1//! # CoqExtraction - Trait Implementations
2//!
3//! This module contains trait implementations for `CoqExtraction`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::CoqExtraction;
12use std::fmt;
13
14impl std::fmt::Display for CoqExtraction {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        match self {
17            CoqExtraction::Language(l) => write!(f, "Extraction Language {}.", l),
18            CoqExtraction::Constant(c, t) => {
19                write!(f, "Extract Constant {} => \"{}\".", c, t)
20            }
21            CoqExtraction::Inductive(c, t) => {
22                write!(f, "Extract Inductive {} => \"{}\" [\"\"].", c, t)
23            }
24            CoqExtraction::Inline(ns) => write!(f, "Extraction Inline {}.", ns.join(" ")),
25            CoqExtraction::NoInline(ns) => {
26                write!(f, "Extraction NoInline {}.", ns.join(" "))
27            }
28            CoqExtraction::RecursiveExtraction(n) => {
29                write!(f, "Recursive Extraction {}.", n)
30            }
31            CoqExtraction::Extraction(n, file) => {
32                write!(f, "Extraction \"{}\" {}.", file, n)
33            }
34            CoqExtraction::ExtractionLibrary(n, file) => {
35                write!(f, "Extraction Library {} \"{}\".", n, file)
36            }
37        }
38    }
39}
oxilean_codegen/coq_backend/coqextraction_traits.rs

oxilean_codegen/coq_backend/
coqextraction_traits.rs
