minitt 0.4.3

Mini-TT, a dependently-typed lambda calculus, extended and (re)implemented in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

use super::{check_declaration_main, check_main};
use crate::ast::{Declaration, Expression, Pattern};

#[test]
fn simple_check() {
    check_declaration_main(Declaration::simple(
        Pattern::Unit,
        vec![],
        Expression::Type(0),
        Expression::One,
    ))
    .unwrap();
    let error_message = check_declaration_main(Declaration::simple(
        Pattern::Unit,
        vec![],
        Expression::Type(0),
        Expression::Unit,
    ))
    .unwrap_err();
    println!("{}", error_message);
}

#[test]
fn check_pair() {
    let expr = Expression::Declaration(
        Box::new(Declaration::simple(
            Pattern::Unit,
            vec![],
            Expression::One,
            Expression::Second(Box::new(Expression::Pair(
                Box::new(Expression::Unit),
                Box::new(Expression::Unit),
            ))),
        )),
        Box::new(Expression::Void),
    );
    check_main(expr).unwrap();
}