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: May 02 2025 at 03:31 UTC