§ Autocompletion in Lean4



$ elan toolchain add my-lean-copy /path/to/my-lean-copy/build/stage0
$ elan override my-lean-copy