logicaffeine-kernel 0.9.16

Pure Calculus of Constructions type theory - NO LEXICON
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

//! Vernacular commands for interacting with the Kernel.

use crate::Term;

/// A command in the Vernacular language.
#[derive(Debug, Clone)]
pub enum Command {
    /// Definition name : type := body.
    ///
    /// If `ty` is None, the type is inferred from the body.
    /// If `is_hint` is true, register as a hint for auto tactic.
    Definition {
        name: String,
        ty: Option<Term>,
        body: Term,
        is_hint: bool,
    },

    /// Check term.
    ///
    /// Prints the type of the term.
    Check(Term),

    /// Eval term.
    ///
    /// Normalizes and prints the term.
    Eval(Term),

    /// Inductive Name (params) := C1 : T1 | C2 : T2.
    ///
    /// Defines an inductive type with its constructors.
    /// Supports optional type parameters for polymorphic inductives.
    Inductive {
        name: String,
        /// Type parameters: (param_name, param_type)
        /// e.g., for `List (A : Type)`, params = [("A", Type)]
        params: Vec<(String, Term)>,
        sort: Term,
        constructors: Vec<(String, Term)>,
    },
}