[Agda] proofs for binary conversion
mechvel at botik.ru
Mon Dec 2 16:14:25 CET 2013
I wrote earlier about
an Agda proof for suc - isomorphism between ℕ and its binary codes
Now, for the occasion that anybody looked there:
I have updated it with a bit simplified version.
The drawback was that I used the ...List.Pointwise equality on Bin⁺
and the construct
b=b' ∷p bs=bs
to build an equality proof for bit lists. This was awkward, because the
Bit equality is syntactical. But I somehow failed to use _≡_ for Bin⁺,
and suffered of complication.
Finally, I recall of the possibility of PropEq.cong₂ _∷_.
Now, this enables to plainly use
_≡_ and PropEq.cong₂ _∷_ b=b' bs=bs'.
More information about the Agda