在学习Programming Language Foundations in Agda第一章Naturals时, 最后有个比特串的反向编码, 觉得也挺有意思的.
data Bin : Set where
nil : Bin
x0_ : Bin → Bin
x1_ : Bin → Bin
编码方式, nil是高位方向
1011 => x1 x1 x0 x1 nil
001011 => x1 x1 x0 x1 x0 x0 nil
这种编码方式用来实现inc(加1)比较简单:
inc : Bin → Bin
inc nil = x1 nil
inc (x0 m) = x1 m
inc (x1 m) = x0 (inc m)
思路很简单, 开始遇到的1都变成0, 最后一个0变为1(在这里面就是第一个0).
