Zulip Chat Archive
Stream: general
Topic: tactic to change transparency?
Scott Morrison (Jul 25 2020 at 01:59):
Is there a tactic to temporarily set the reducibility of a definition?
Reid Barton (Jul 25 2020 at 02:01):
docs#tactic.with_local_reducibility
Last updated: Aug 03 2023 at 10:10 UTC