bluespec - 关于附带条件的澄清

Question

我正在研究 Bluespec System Verilog。

在 Shakti 处理器的源代码中，我找到了这个模块定义：

 module mkuart_user#(parameter Bit#(16) baudrate)
 (UserInterface#(addr_width,data_width, depth))
      provisos(
        Add#(a__, 8, data_width),
        Add#(b__, 16, data_width),
        Mul#(16, c__, data_width),
        Mul#(8, d__, data_width),
        Add#(2, e__, depth)
      );
...some code....

我不明白怎么

Add# and Mul# provisos work in this case.

从语言文档中我了解到

Add#(a__,8,data_width) means a__ + 8 = data_width 

and 

Mul#(16,c__,data_width)means 16 * c__ = data_width

但是 a__ 和 c__ 来自哪里？我到处寻找，我什么也没找到。