Zulip Chat Archive
Stream: lean4
Topic: Is there a way to build proof interactively
Lim, Thing-han (Mar 04 2021 at 03:29):
Is there a way to build proof interactively like agda hole in Lean 4 ?
Bryan Gin-ge Chen (Mar 04 2021 at 03:32):
Not yet, but it should be possible after "hole commands" are implemented in the Lean 4 server.
Lim, Thing-han (Mar 04 2021 at 03:41):
Understand, thank you !
Last updated: May 02 2025 at 03:31 UTC