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
21
22
23

/// Normalised, verified form of introduction commands.
///
/// An introduction command can have many shapes:
/// `x: A`, `x := t`, `x: A := t`, ...
/// A typing provides a uniform presentation of introduction commands
/// with respect to type checking.
#[derive(Clone)]
pub struct Typing<Ty, Tm = Ty> {
    /// local context
    pub lc: alloc::vec::Vec<Ty>,
    pub ty: Ty,
    pub tm: Tm,
}

impl<Ty, Tm> Typing<Ty, Tm> {
    pub fn new(ty: Ty, tm: Tm) -> Self {
        Self {
            lc: Default::default(),
            ty,
            tm,
        }
    }
}