Enum Command 

pub enum Command {
    Definition {
        name: String,
        ty: Option<Term>,
        body: Term,
        is_hint: bool,
        implicit_count: usize,
    },
    Check(Term),
    Eval(Term),
    Inductive {
        name: String,
        params: Vec<(String, Term)>,
        sort: Term,
        constructors: Vec<(String, Term)>,
    },
}

A command in the Vernacular language.

Variants

Definition

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.

Fields

name: String

ty: Option<Term>

body: Term

is_hint: bool

implicit_count: usize

How many leading parameters of ty are implicit ({x:T} binders).

Check(Term)

Check term.

Prints the type of the term.

Eval(Term)

Eval term.

Normalizes and prints the term.

Inductive

Inductive Name (params) := C1 : T1 | C2 : T2.

Defines an inductive type with its constructors. Supports optional type parameters for polymorphic inductives.

Fields

name: String

params: Vec<(String, Term)>

Type parameters: (param_name, param_type) e.g., for List (A : Type), params = [(“A”, Type)]

sort: Term

constructors: Vec<(String, Term)>

Trait Implementations

impl Clone for Command

fn clone(&self) -> Command

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Command

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.