oxilean_codegen/agda_backend/
agdapattern_traits.rs1use super::types::AgdaPattern;
12use std::fmt;
13
14impl fmt::Display for AgdaPattern {
15 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16 match self {
17 AgdaPattern::Var(x) => write!(f, "{}", x),
18 AgdaPattern::Con(c, args) => {
19 if args.is_empty() {
20 write!(f, "{}", c)
21 } else {
22 write!(f, "({}", c)?;
23 for a in args {
24 write!(f, " {}", a)?;
25 }
26 write!(f, ")")
27 }
28 }
29 AgdaPattern::Wildcard => write!(f, "_"),
30 AgdaPattern::Num(n) => write!(f, "{}", n),
31 AgdaPattern::Dot(p) => write!(f, ".{}", p),
32 AgdaPattern::Absurd => write!(f, "()"),
33 AgdaPattern::As(x, p) => write!(f, "{}@{}", x, p),
34 AgdaPattern::Implicit(p) => write!(f, "{{{}}}", p),
35 }
36 }
37}