lean
lean copied to clipboard
The after_set field of user attributes does not have access to current options
See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/options.20in.20user.20attributes