F5でデバッグモードはできない

vscode Lean

コード編集中に[F5]でデバッグモードになるが、Leanの場合は、デバッガやそのVSCode拡張が存在しないので、[F5]は効かない。