Commit 2023-03-16 04:49 b05549b3
View on Github →feat: port @[elementwise]
attribute (#2882)
This ports the @[elementwise]
attribute and the elementwise_of% e
term elaborator.
It does not port the elementwise! h
tactic, which can instead be handled by replace h := elementwise_of% h
for now.