[Agda] Nat -iso- Bin

[Sergei Meshveliani]

Correction:  ``{m : ℕ} → ''  
is not needed here.

Also there is a question about availability of  fromℕ ∘ toℕ ≗ id,
fromDigits ∘ toDs ≗ id.


On Tue, 2013-10-29 at 22:51 +0400, Sergei Meshveliani wrote:
> Please, has  lib-0.7  something for the isomorphism  ℕ <-> Bin ?
> 
> For example, I need 
> 
>   toDigits-suc-eq : {m : ℕ} → 
>                     let toDs : ℕ → Bin⁺
>                         toDs = proj₁ ∘ toDigits 2                    
>                     in 
>                     toDs ∘ suc ≗ (addCarryToBitList 1b ∘ toDs) 
> 
> Probably,      fromℕ ∘ suc ≗ Bin.suc ∘ fromℕ 
> will also do.
> 
> I think of proving  toDigits-suc-eq,  but this needs looking into a
> non-trivial definition of  toDigits.
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>