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::*;

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

/**
Meta variable solving,
term (definitional) equality comparison.
*/
mod unify;

/// Declaration relevant checking.
///
/// Depends on `expr`.
mod decl;
/**
Tooling functions that depends on neither `decl` nor `expr`.
*/
mod eval;
/**
$$
\\newcommand{\\xx}[0]{\\texttt{x}}
\\newcommand{\\istype}[0]{\\vdash_\\texttt{t}}
\\newcommand{\\Gistype}[0]{\\Gamma \\istype}
\\newcommand{\\tyck}[0]{\\vdash_\\texttt{c}}
\\newcommand{\\Gtyck}[0]{\\Gamma \\tyck}
\\newcommand{\\infer}[0]{\\vdash_\\texttt{i}}
\\newcommand{\\Ginfer}[0]{\\Gamma \\infer}
\\newcommand{\\subtype}[0]{\\vdash_{<:}}
\\newcommand{\\Gsubtype}[0]{\\Gamma \\subtype}
\\newcommand{\\ty}[0]{\\textsf{Type}}
\\newcommand{\\Sum}[0]{\\texttt{Sum}\\ }
\\newcommand{\\merge}[0]{\\texttt{merge}}
\\newcommand{\\inst}[0]{\\texttt{inst}}
\\newcommand{\\ctor}[0]{\\texttt{cons}\\ }
\\newcommand{\\app}[0]{\\texttt{app}}
\\newcommand{\\first}[0]{\\texttt{first}}
\\newcommand{\\second}[0]{\\texttt{second}}
\\Gistype a \\Rightarrow o
\\quad
\\Ginfer a \\Rightarrow o
\\quad
\\Gtyck a:m \\Rightarrow o
$$
Expression/Type relevant checking.
*/
mod expr;