The Coq mailing list

["Joan Josep Jim�nez Puig" <jumi99 AT gmail.com>]

Hi, 
first of all apologies for my english :) I'm reading the Coq'Art book and there's
one exercise I cannot solve. It is from chapter 6, Dependent Inductive Types.

I have defined a type (binary_word : nat -> Set) of strings of bits of a known length.
The exercise is to compute the bit-wise "or" of two binary_words.

Here's the code I've done, but it doesn't work because in the recursive call
there's a problem with the parameter n. If I put x it will complain
about the type of bw2' and if i put x' it will complain about bw1'.
I have to use somehow the fact that x=x', but I don't know how to do it.

Inductive binary_word : nat -> Set :=
  |F : binary_word O
  |M : forall n:nat, Bit -> binary_word n -> binary_word (S n).

Fixpoint binary_word_or (n:nat) (bw1:binary_word n)
                                (bw2:binary_word n) {struct bw1}
         : binary_word n :=
   match bw1 in binary_word q return binary_word q with
      | F => F
      | M x b bw1' =>
         match bw2 in binary_word q return binary_word q with
            | F => F
            | M x' b2 bw2' =>
               M x (bit_or b b2) (binary_word_or x bw1' bw2')
         end
   end.

Thanks.