minitt 0.1.9

Mini-TT, a dependently-typed lambda calculus, implementated 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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

/*!

Reading the [README](https://github.com/owo-lang/minitt-rs/blob/master/README.md) is recommended
before reading the documentation.
*/

/// Reduction: eval and eval's friends.
///
/// Functions in this module are put into `impl` blocks, their docs can be found in:
///
/// + [Methods of `Pattern`](../syntax/enum.Pattern.html#methods)
/// + [Methods of `Value`](../syntax/enum.Value.html#methods)
/// + [Methods of `Telescope`](../syntax/enum.Telescope.html#methods)
/// + [Methods of `Closure`](../syntax/enum.Closure.html#methods)
/// + [Methods of `Expression`](../syntax/enum.Expression.html#methods)
///
/// Depends on module `syntax`.
pub mod reduce;
/// Syntax: term, expression, context.
///
/// Methods are defined in `reduce`/`read_back` modules but their documents are here.
///
/// No dependency.
pub mod syntax;

/// Normal form: when we read back, we get a normal form expression.
///
/// Depends on module `syntax`.
pub mod normal;
/// Read back: read back functions.
///
/// Converting terms to normal forms with de-bruijn indices so
/// we do not need to deal with alpha conversions.
///
/// Functions in this module are put into `impl for` blocks, their docs can be found in:
///
/// + [`ReadBack` of `Value`](../syntax/enum.Value.html#impl-ReadBack)
/// + [`ReadBack` of `Telescope`](../syntax/enum.Telescope.html#impl-ReadBack)
/// + [`ReadBack` of `Closure`](../syntax/enum.Closure.html#impl-ReadBack)
///
/// Depends on modules `syntax` and `normal`.
pub mod read_back;

/// Type checking: the four type checking functions -- `checkI`, `checkD`, `check` and `checkT`.
///
/// Depends on modules `syntax`, `normal`, `reduce` and `read_back`.
pub mod type_check;

/// Pretty print utilities
#[cfg(feature = "pretty")]
pub mod pretty;

/// Parser, from text to AST and a bunch of utilities
#[cfg(feature = "parser")]
pub mod parser;