logicaffeine_kernel/interface/
command.rs

1//! Vernacular commands for interacting with the Kernel.
2
3use crate::Term;
4
5/// A command in the Vernacular language.
6#[derive(Debug, Clone)]
7pub enum Command {
8    /// Definition name : type := body.
9    ///
10    /// If `ty` is None, the type is inferred from the body.
11    /// If `is_hint` is true, register as a hint for auto tactic.
12    Definition {
13        name: String,
14        ty: Option<Term>,
15        body: Term,
16        is_hint: bool,
17    },
18
19    /// Check term.
20    ///
21    /// Prints the type of the term.
22    Check(Term),
23
24    /// Eval term.
25    ///
26    /// Normalizes and prints the term.
27    Eval(Term),
28
29    /// Inductive Name (params) := C1 : T1 | C2 : T2.
30    ///
31    /// Defines an inductive type with its constructors.
32    /// Supports optional type parameters for polymorphic inductives.
33    Inductive {
34        name: String,
35        /// Type parameters: (param_name, param_type)
36        /// e.g., for `List (A : Type)`, params = [("A", Type)]
37        params: Vec<(String, Term)>,
38        sort: Term,
39        constructors: Vec<(String, Term)>,
40    },
41}
logicaffeine_kernel/interface/command.rs

logicaffeine_kernel/interface/
command.rs
