In this snippet ```fstar let f ([@@@"attr"] x y : int) = 1 ``` the attribute is only on `x`. This looks confusing to me, is it intended? One can add the attribute to both binders like this: ```fstar let f ([@@@"attr"] x [@@@"attr"] y : int) = 1 ```