batteries
batteries copied to clipboard
feat: `trySetOptions` / `tryEraseAttrs` command elab helpers
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.