oxilean-std 0.1.2

OxiLean standard library
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use super::functions::*;
use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};

#[cfg(test)]
mod tests {
    use super::*;
    use oxilean_kernel::Environment;
    #[test]
    fn test_build_real_env() {
        let mut env = Environment::new();
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Eq"),
            univ_params: vec![],
            ty: pi(
                BinderInfo::Implicit,
                "_",
                type0(),
                pi(
                    BinderInfo::Default,
                    "_",
                    bvar(0),
                    pi(BinderInfo::Default, "_", bvar(1), prop()),
                ),
            ),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("And"),
            univ_params: vec![],
            ty: arrow(prop(), arrow(prop(), prop())),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Or"),
            univ_params: vec![],
            ty: arrow(prop(), arrow(prop(), prop())),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Iff"),
            univ_params: vec![],
            ty: arrow(prop(), arrow(prop(), prop())),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Not"),
            univ_params: vec![],
            ty: arrow(prop(), prop()),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Exists"),
            univ_params: vec![],
            ty: pi(
                BinderInfo::Implicit,
                "a",
                type0(),
                arrow(arrow(bvar(0), prop()), prop()),
            ),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Nat"),
            univ_params: vec![],
            ty: type0(),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Nat.zero"),
            univ_params: vec![],
            ty: nat_ty(),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Nat.succ"),
            univ_params: vec![],
            ty: arrow(nat_ty(), nat_ty()),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Nat.add"),
            univ_params: vec![],
            ty: arrow(nat_ty(), arrow(nat_ty(), nat_ty())),
        });
        let _ = env.add(Declaration::Axiom {
            name: Name::str("Nat.mul"),
            univ_params: vec![],
            ty: arrow(nat_ty(), arrow(nat_ty(), nat_ty())),
        });
        let result = build_real_env(&mut env);
        assert!(result.is_ok(), "build_real_env failed: {:?}", result);
    }
    #[test]
    fn test_real_expression_builders() {
        let a = cst("a");
        let b = cst("b");
        let sum = real_add(a.clone(), b.clone());
        assert!(matches!(sum, Expr::App(_, _)));
        let prod = real_mul(a.clone(), b.clone());
        assert!(matches!(prod, Expr::App(_, _)));
        let neg = real_neg(a.clone());
        assert!(matches!(neg, Expr::App(_, _)));
        let inv = real_inv(a.clone());
        assert!(matches!(inv, Expr::App(_, _)));
        let _abs = real_abs(a.clone());
        assert!(matches!(_abs, Expr::App(_, _)));
        let le = real_le(a.clone(), b.clone());
        assert!(matches!(le, Expr::App(_, _)));
        let zero = real_zero();
        assert!(matches!(zero, Expr::Const(_, _)));
        let one = real_one();
        assert!(matches!(one, Expr::Const(_, _)));
        let dist = real_dist(a, b);
        assert!(matches!(dist, Expr::App(_, _)));
    }
}