Commit 2022-03-08 09:02 900e55a8

View on Github →

fix: auto-bounds should be parameters, not indices (#220) See: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20implicit.20argument.20inference

Estimated changes

Modified Mathlib/Data/List/Perm.lean

modified inductive List.Perm

Modified Mathlib/Init/Data/List/Lemmas.lean

modified inductive List.sublist