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        /// How many leading parameters of `ty` are implicit (`{x:T}` binders).
18        implicit_count: usize,
19    },
20
21    /// Check term.
22    ///
23    /// Prints the type of the term.
24    Check(Term),
25
26    /// Eval term.
27    ///
28    /// Normalizes and prints the term.
29    Eval(Term),
30
31    /// Inductive Name (params) := C1 : T1 | C2 : T2.
32    ///
33    /// Defines an inductive type with its constructors.
34    /// Supports optional type parameters for polymorphic inductives.
35    Inductive {
36        name: String,
37        /// Type parameters: (param_name, param_type)
38        /// e.g., for `List (A : Type)`, params = [("A", Type)]
39        params: Vec<(String, Term)>,
40        sort: Term,
41        constructors: Vec<(String, Term)>,
42    },
43}
logicaffeine_kernel/interface/command.rs

logicaffeine_kernel/interface/
command.rs
