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: Feb 28 2026 at 14:05 UTC