Module interface 

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.