[Agda] Problem with inductively defined type having (simulated) partial constructors

[Wouter Swierstra]

Hi Tristan,

>> The other problem with your code is that it isn't obviously
>> structurally recursive, and therefore doesn't termination check. This
>> surprised me a bit. It seems ok, but maybe I'm missing something  
>> here.

Dan Licata just pointed out that once you solve all the missing  
proofs, the termination checker stops complaining. Phew.

> allzeros                                                 === 00000000b
> allzeros orone                                           === 00000001b
> allzeros orone shifted                                   === 00000010b
> allzeros orone shifted orone                             === 00000011b
> allzeros orone shifted shifted                           === 00000100b
> allzeros orone shifted orone                             === 00000101b
> allzeros orone shifted orone shifted                     === 00000110b
> allzeros orone shifted orone shifted orone               === 00000111b
> allzeros orone shifted shifted shifted                   === 00001000b

What about:

data Word : Nat -> Set where
   Nil : Word 0
   Cons : {n : Nat} -> Bit -> Word n -> Word (Succ n)

data Fin : Nat -> Set where
   Fz : {n : Nat} -> Fin (Succ n)
   Fs : {n : Nat} -> Fin n -> Fin (Succ n)

Octet = Word 8

And then defining:

or : {n : Nat} Word n -> Word n -> Word n

shift : {n : Nat} -> Fin n -> Word n -> Word n
-- or
shift : {n : Nat} -> (k : Nat) -> ((k < n) IsTrue) -> Word n -> Word n

Is there any particular reason you want exactly this inductive  
structure for the Octet type? Just curious,

   Wouter