feat: further @[grind] annotations for Option
#13111
copyright-header.yml
on: pull_request
check-lean-files
32s
@[grind] annotations for Option
#13111