truncate has wrong provisos in the BSC libraries reference guide documentation

[pbing]

The provisos wrongly asserts m >= n

function x#(m) truncate (x#(n) d)
   provisos (Add#(k, n, m));

Probably a typo because the bit width of the function argument and function result is swapped at the same time as the provisos arguments.
The provisos should be:

function x#(m) truncate (x#(n) d)
   provisos (Add#(k, m, n));

Here is the source code of the BitExtend functions and their description in the documentation.

Prelude.bs:

primitive primZeroExt :: (Add k n m) => Bit n -> Bit m

primitive primSignExt :: (Add k n m) => Bit n -> Bit m

primitive primTrunc :: (Add k m n) => Bit n -> Bit m

PreludeBSV.bsv:

function Bit#(n) truncateLSB(Bit#(m) x)
   provisos(Add#(n,k,m));

bsc_libraries_ref_guide.pdf:

function x#(n) zeroExtend (x#(m) d)
   provisos (Add#(k, m, n));

function x#(n) signExtend (x#(m) d)
   provisos (Add#(k, m, n));

function x#(m) truncate (x#(n) d)
   provisos (Add#(k, n, m)); // wrong

function Bit#(n) truncateLSB(Bit#(m) x)
   provisos(Add#(n,k,m));

[quark17]

Thank you. I agree that the fix is to keep the proviso the same as on all the other functions in the group. I will submit a PR to fix that, thanks.

The presentation in that section is a little loose: there is no actual Add proviso in the declaration of the member function, but that proviso will be added when the function is used, so the documentation is probably trying to keep things simple for users (who may not fully understand typeclasses yet). If the BitExtend typeclass declaration had an Add proviso, it might easy to explain to the user where the proviso is coming from. But BSC currently doesn't allow this (due to issue #633), so instead every instance of BitExtend needs to have the Add proviso to make up for it.