Expand description
Interactive REPL driver for panproto theories, terms, and morphisms.
The binary (panproto-repl) wires Repl::handle_line to
rustyline. Tests drive the same entry point with a scripted input
stream so no terminal is required.
§Commands
Commands start with :. Bare input (no leading :) is treated as a
term to typecheck in the active theory.
:load <path>: load a theory document.:theories: list loaded theories.:use <name>: switch the active theory.:sorts,:ops: list the active theory’s sorts and ops.:type <term>: infer the sort of a term.:normalize <term>: normalize a term under the active theory’s directed equations.:model [depth]: print terms in each fiber from the active theory’s free model.:instance <class> in <target> { <bindings> }: compile an ad-hoc instance morphism.:quit/:q: leave the REPL.
Structs§
- Repl
- The REPL driver state. Holds loaded theories, the currently active theory name, and any compiled morphisms.
Enums§
- Repl
Outcome - Outcome of processing a single line.