lean icon indicating copy to clipboard operation
lean copied to clipboard

The after_set field of user attributes does not have access to current options

Open fpvandoorn opened this issue 5 years ago • 0 comments

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/options.20in.20user.20attributes

fpvandoorn avatar Mar 05 '21 04:03 fpvandoorn