Module interface 

Re-export of the LOGOS interface types from the kernel crate.

Provides access to core types like World and Entity for integration with the LOGOS runtime. Vernacular interface for the Kernel.

Provides a text-based command interface for interacting with the kernel:

• Definition name : type := term. - Add a definition
• Check term. - Print the type of a term
• Eval term. - Normalize and print a term
• Inductive Name := C1 : T1 | C2 : T2. - Define an inductive type

Literate Syntax (English-like alternative)

• A Bool is either Yes or No. - Define an inductive type
• ## To add (n: Nat) and (m: Nat) -> Nat: - Define a function
• Consider x: When Zero: Yield m. - Pattern matching

Modules

literate_parser

Literate Specification Parser for the Kernel.

Structs

Repl

The Vernacular REPL.

TermParser

Recursive descent parser for Term syntax.

Enums

Command

A command in the Vernacular language.

InterfaceError

Errors that can occur in the interface layer.

ParseError

Parse errors for the Vernacular.

Functions

parse_command

Parse a command from input string.