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: May 16 2021 at 05:21 UTC