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() -> Repl

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 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() -> Repl

Returns the “default value” for a type.