Now binport will apply the @[to_additive] attribute corresponding to lean 3 tagged definitions, which is helpful if you want to use the lean 4 @[to_additive] on top of binported oleans. Synport will use the information to display double #align statements for declarations with the @[to_additive] attribute.
Now binport will apply the
@[to_additive]attribute corresponding to lean 3 tagged definitions, which is helpful if you want to use the lean 4@[to_additive]on top of binported oleans. Synport will use the information to display double#alignstatements for declarations with the@[to_additive]attribute.