Zulip Chat Archive

Stream: new members

Topic: case-split in emacs mode?

Jason Gross (Mar 05 2021 at 18:49):

Is there a way to get emacs to insert a case split for me, a la match! of company-coq or C-c C-s of Agda's emacs mode?

Johan Commelin (Mar 05 2021 at 19:12):

In Lean3 there are hole commands. No idea whether they are implemented for Lean4 already

Jason Gross (Mar 05 2021 at 19:19):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Is.20there.20a.20way.20to.20build.20proof.20interactively/near/228710628 suggests that they are not, alas. Thanks for the pointer, though!

Last updated: Dec 20 2023 at 11:08 UTC