Zulip Chat Archive
Stream: mathlib4
Topic: Nonparametric `induction`
Martin Dvořák (Oct 27 2023 at 09:14):
I have a feature request: What about defining induction without parameters to mean the following?
intro n
induction n with
ZHAO Jiecheng (Oct 31 2023 at 06:54):
(deleted)
Last updated: Dec 20 2023 at 11:08 UTC