Struct Repl 

pub struct Repl { /* private fields */ }

The Vernacular REPL.

Maintains a kernel context and executes commands against it.

Implementations

impl Repl

pub fn new() -> Self

Create a new REPL with the standard library loaded.

pub fn execute(&mut self, input: &str) -> Result<String, InterfaceError>

Execute a command string.

Returns the output string (for Check/Eval) or empty string (for Definition/Inductive).

pub fn execute_batch( &mut self, inputs: &[String], ) -> Vec<Result<String, InterfaceError>>

Execute a batch of Vernacular commands, recovering mutual-inductive grouping.

execute registers each Inductive independently, so a forward reference between two separately-declared inductives — Tree whose Node constructor mentions Forest, declared next — fails: Forest is not yet in scope when Tree’s constructor is universe-checked. True mutual inductives must be registered together, through the trusted Context::add_mutual_inductives, which runs whole-block positivity and a header-first universe check.

This entry point recovers that grouping from a flat statement sequence: a maximal run of consecutive Inductive commands is split into strongly-connected components of the “a constructor mentions sibling b” graph. A genuine cycle (Tree↔Forest) is registered as one mutual block; an acyclic reference (Leafy → Bare) becomes two singletons registered dependency-first (Bare, then Leafy) through the ordinary single-inductive path. Every non-inductive command — and every inductive with no forward reference — runs exactly as execute would, in source order, so a batch without forward references is byte-identical to running the statements singly.

pub fn context(&self) -> &Context

Get a reference to the underlying context.

pub fn context_mut(&mut self) -> &mut Context

Get a mutable reference to the underlying context.

Trait Implementations

impl Default for Repl

fn default() -> Self

Returns the “default value” for a type.