比特串from的括号问题

我的from函数

from : Bin → ℕ
from nil    = zero
from (x0 m) = 2 * from m
from (x1 m) = 1 + (2 * from m)

我怀疑是有问题的, 但是实际操作起来是这样的

f = 3 * 4 * 5 -- error, 需要括号
Could not parse the application 3 * 4 * 5
Operators used in the grammar:
  * (infix operator, level 20) [_*_ (/Users/zhang/Desktop/Haskell/Agda/Naturals.agda:17,1-4)]
when scope checking 3 * 4 * 5

-- _ : from (x1_ (x0_ (x1_ nil))) ≡ 5
_ =
  begin
    from (x1_ (x0_ (x1_ nil)))
  ≡⟨⟩
    1 + (2 * from (x0 (x1_ nil)))
  ≡⟨⟩
    1 + (2 * (2 * from (x1_ nil))) -- Agda会自己加括号的呢
  ≡⟨⟩
    1 + (2 * (2 * (1 + (2 * from nil))))
  ≡⟨⟩
    1 + (2 * (2 * (1 + (2 * zero))))
  ≡⟨⟩
    1 + (2 * (2 * (1 + 0)))
  ≡⟨⟩
    5
  ∎

Agda的constructor到底是怎么做到的呢?

它不仅可以用已有元素去构造新元素, 还能从已有元素中得到构造其的元素.

现在不要去想, 不用去想, 保持愚蠢.