我的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到底是怎么做到的呢?
它不仅可以用已有元素去构造新元素, 还能从已有元素中得到构造其的元素.
现在不要去想, 不用去想, 保持愚蠢.
