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.