Zulip Chat Archive
Stream: lean4
Topic: Induction code_action for fun_induction
Shreyas Srinivas (Nov 14 2025 at 13:50):
Currently the code action of induction doesn't work for fun_induction. Could we make this work?
Last updated: Dec 20 2025 at 21:32 UTC