logicaffeine_kernel/interface/mod.rs
1//! Vernacular interface for the Kernel.
2//!
3//! Provides a text-based command interface for interacting with the kernel:
4//! - `Definition name : type := term.` - Add a definition
5//! - `Check term.` - Print the type of a term
6//! - `Eval term.` - Normalize and print a term
7//! - `Inductive Name := C1 : T1 | C2 : T2.` - Define an inductive type
8//!
9//! # Literate Syntax (English-like alternative)
10//!
11//! - `A Bool is either Yes or No.` - Define an inductive type
12//! - `## To add (n: Nat) and (m: Nat) -> Nat:` - Define a function
13//! - `Consider x: When Zero: Yield m.` - Pattern matching
14
15mod command;
16mod command_parser;
17mod error;
18pub mod literate_parser;
19mod repl;
20mod term_parser;
21
22pub use command::Command;
23pub use command_parser::parse_command;
24pub use error::{InterfaceError, ParseError};
25pub use repl::Repl;
26pub use term_parser::TermParser;