Zulip Chat Archive

Stream: lean4

Topic: Use lean in jupyter

zhipeng (Jul 18 2023 at 01:04):

I guess it is more convenient to use lean in jupyter or vacode, so if is possible to use lean in jupyter?

zhipeng (Jul 18 2023 at 01:08):

zhipeng said:

I guess it is more convenient to use lean in jupyter or vacode, so if is possible to use lean in jupyter?

Maybe it is a wrong question, in vscode I can see the goal in time

Miguel Marco (Jul 18 2023 at 13:01):

See here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Prototype.3A.20Jupyter.20for.20Lean4/near/347820222

Last updated: Dec 20 2023 at 11:08 UTC