kontroli 0.4.0

Type checking for the lambda-Pi calculus modulo rewriting
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

use alloc::vec::Vec;
use core::fmt::{self, Display};

/// Command that changes the global context.
#[derive(Clone)]
pub enum Command<Id, Intro, Rule> {
    /// Introduce a new name
    Intro(Id, Intro),
    /// Add rewrite rules
    Rules(Vec<Rule>),
}

impl<Id: Display, Intro: Display, Rule: Display> Display for Command<Id, Intro, Rule> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            Self::Intro(id, it) => write!(f, "{} {}", id, it),
            Self::Rules(rules) => rules.iter().try_for_each(|r| r.fmt(f)),
        }
    }
}