Skip to main content

ratex_parser/functions/
bussproofs.rs

1use std::collections::HashMap;
2
3use crate::error::ParseResult;
4use crate::functions::{define_function_full, FunctionContext, FunctionSpec};
5use crate::parse_node::{AtomFamily, ParseNode};
6
7pub fn register(map: &mut HashMap<&'static str, FunctionSpec>) {
8    define_function_full(
9        map,
10        &["\\fCenter"],
11        "internal",
12        0,
13        0,
14        None,
15        true,
16        true,
17        true,
18        false,
19        false,
20        handle_fcenter,
21    );
22}
23
24fn handle_fcenter(
25    ctx: &mut FunctionContext,
26    _args: Vec<ParseNode>,
27    _opt_args: Vec<Option<ParseNode>>,
28) -> ParseResult<ParseNode> {
29    // bussproofs defaults \fCenter to \Rightarrow (U+21D2 ⇒), separating the
30    // left and right sides of a sequent (e.g. A \fCenter B → "A ⇒ B").
31    Ok(ParseNode::Atom {
32        mode: ctx.parser.mode,
33        family: AtomFamily::Rel,
34        text: "\\Rightarrow".to_string(),
35        loc: None,
36    })
37}