まぁ、動いてはいるんですけどね
なんか、知らんけど
引数がずれる
goal 表示する時に、隣のを表示してしまうんだな。まぁ、害はない
前に使っていたのは「sub windowが出て表示する方式」だったんだが、こっちは「Windowを割って表示する」
まぁ、どっちでも。あと、term が表示が少し変。まあ、それも害はない
自分で作って使うと「そういうの気にならない」ところがあってさ、まぁ、そうなんでしょう
正気な人は VSCode を使っているんだろうとは思うんだけど
Lean は VSCode only らしい
自分の手元のを Lean に書き換えようって気もなくはないんですけどね
https://github.com/isovector/cornelis.git
No comments:
Post a Comment