>
Enter: run
โข Shift+Enter: newline
โข Tab: autocomplete
โข โ/โ: history
โข Ctrl+L: clear
โข Drag & drop .k/.klib files anywhere
| Codec Name | Target Type Binding | Capabilities | Source | Action |
|---|
(text, context) => Value
(value, context) => string
:load <file> | Load a .k source or .klib library into current state |
:t <name> | Display the derived type of relation <name> |
:d <name> | Display definition of relation <name> |
:type <name> | Show or define a type (:type name = <...>) |
:rel <name> = expr | Define a relation alias |
:codes | List all type aliases |
:rels | List all relation aliases |
:codecs | List all loaded codecs / serializers |
:codec load <name|file> | Load a built-in codec (int, utf8, json, ieee) or file |
:codec define n t b | Define inline custom codec: name type { parse: ..., print: ... } |
:codec unload <name> | Unload a registered codec |
:input <type> [codec] | Read next input line using specified codec |
:val | Print current accumulator value |
:klib <file> | Export current state as a .klib binary file |
:reset | Clear state and reset to initial environment |
:help | Show command reference |
Any raw K expression entered at the prompt is compiled and evaluated on top of the current state using WebAssembly.
10 — Integer literal (encodes to bit-path via arithmetics){10 int x, 5 int y} plus — Composition / function callsucc = {inv x, _ y} _inc; — Define a relation (ends with ;)$ bit = < {} 0, {} 1 >; — Define a typeEnter | Execute if snippet is complete, otherwise insert newline |
Shift+Enter | Insert newline without executing |
Ctrl+Enter / Cmd+Enter | Force execute whatever is in input |
Tab | Autocomplete commands, aliases, and filenames |
โ / โ | Navigate command history |
Ctrl+L | Clear terminal output |
Esc | Dismiss autocomplete / clear input |