Zulip Chat Archive
Stream: mathlib4
Topic: Placeholder in obtain
Yaël Dillies (Apr 24 2023 at 08:12):
Does obtain not accept placeholders anymore/is much more strict about where they can be? This came up here and I cannot minimize. All my MWEs do work.
Last updated: May 02 2025 at 03:31 UTC