batteries chore: 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead

chore: 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead

Open jcommelin opened this issue 2 years ago • 2 comments

Dec 01 '23 09:12 jcommelin

I've set this back to awaiting-review. I am keen to have this in.

Dec 14 '23 21:12 kim-em

Superseded by #625

Jul 23 '24 11:07 fgdorais

Since #625 has been merged, this can now certainly be closed.

Aug 19 '24 06:08 jcommelin