batteries icon indicating copy to clipboard operation
batteries copied to clipboard

feat: `trySetOptions` / `tryEraseAttrs` command elab helpers

Open tydeu opened this issue 7 months ago • 8 comments

Helpers which I wrote for @hrmacbeth to use in her Mechanics of Proof package to help with initializing options and attributes for a teaching environment. She suggested I PR these helpers to Std as they quite helpful when configuring custom environments and are thus useful to many who teach Lean.

tydeu avatar Jan 07 '24 22:01 tydeu