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: Dec 20 2023 at 11:08 UTC