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

pub use self::decl::*;
pub use self::eval::*;
pub use self::expr::*;
pub use self::unify::*;

/**
Type-checking monad is a `Result<State, Error>`.
$$
\\newcommand{\\xx}[0]{\\texttt{x}}
\\Gamma
\\quad
\\Gamma(\xx)=o
$$
*/
pub mod monad;

/**
Meta variable solving,
term (definitional) equality comparison.
$$
\Gamma \vdash A \simeq B
$$
*/
mod unify;

/**
Declaration relevant checking.
$$
\\newcommand{\\checkD}[0]{\\vdash_\\texttt{d}}
\\newcommand{\\GcheckD}[0]{\\Gamma \\checkD}
\\GcheckD D\ \textbf{ok}
$$

Depends on `expr`.
*/
mod decl;
/**
Tooling functions that depends on neither `decl` nor `expr`.
$$
\llbracket a \rrbracket = \alpha
$$
*/
mod eval;
/**
Expression/Type relevant checking.
$$
\\newcommand{\\tyck}[0]{\\vdash_\\texttt{c}}
\\newcommand{\\Gtyck}[0]{\\Gamma \\tyck}
\\newcommand{\\infer}[0]{\\vdash_\\texttt{i}}
\\newcommand{\\Ginfer}[0]{\\Gamma \\infer}
\\Ginfer a \\Rightarrow o
\\quad
\\Gtyck a:m \\Rightarrow o
\\quad
\\Gamma \vdash A <: B
$$
*/
mod expr;