[Agda] using Induction.Nat

[Sergei Meshveliani]

On Tue, 2013-10-08 at 12:10 +0900, Andreas Abel wrote:
> Using Data.Bin was also my hunch.  Here is a partial solution to your 
> problem:
> 
> [..]

> open import Data.Fin using (zero; suc)
> open import Data.Bin using (Bin⁺; 0#; _1#; fromℕ)
> 
> open import Relation.Binary.PropositionalEquality
> 
> -- Binary exponentiation
> 
> module Power {A : Set} (_•_ : A → A → A) (x : A) where
> 
>    binPower : Bin⁺ → A
>    binPower []       = x


Indeed, using the Bin⁺ argument simplifies the proofs greatly.
Because  (2 *)  converts to  (bit ::),  and termination becomes given
for free.  
So, my introduction to inductive types is delayed to the first future
unlucky case.

Thanks to people!

------
Sergei