feat: add @[grind ext] attributes for extensional maps
#19214
copyright-header.yml
on: pull_request
check-lean-files
22s