oxilean_codegen/coq_backend/
coqattribute_traits.rs1use super::types::CoqAttribute;
12use std::fmt;
13
14impl std::fmt::Display for CoqAttribute {
15 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16 match self {
17 CoqAttribute::Global => write!(f, "#[global]"),
18 CoqAttribute::Local => write!(f, "#[local]"),
19 CoqAttribute::Export => write!(f, "#[export]"),
20 CoqAttribute::Transparent => write!(f, "Transparent"),
21 CoqAttribute::Opaque => write!(f, "Opaque"),
22 CoqAttribute::Polymorphic => write!(f, "#[universes(polymorphic)]"),
23 CoqAttribute::Monomorphic => write!(f, "#[universes(monomorphic)]"),
24 CoqAttribute::Program => write!(f, "Program"),
25 CoqAttribute::Equations => write!(f, "Equations"),
26 CoqAttribute::Custom(s) => write!(f, "#[{}]", s),
27 }
28 }
29}