Skip to main content

Module completions

Module completions 

Source
Expand description

CLI tab-completions: lean-ctx completions <shell> generates a script, lean-ctx __complete <shell> -- <words…> serves dynamic completions.

Modules§

spec
Static command-tree specification for CLI completions.

Functions§

run___complete
lean-ctx __complete zsh -- <words…> — emit completions for the current input.
run_completions
lean-ctx completions zsh|bash|fish — print a static completion script.