The Coq mailing list

["Ly Kim Quyen (Gwenhael)" <lykimq AT gmail.com>]

Hello,

I have a question about an dependent type.

I have a function poly_symbol is:

Fixpoint poly_symbol ( l : list {g: symbol & poly (arity g)}) : poly (arity f) :=
   match l with
   | existT g p :: l' =>

                 match eq_symb_dec f g with
                     | left h => poly_cast h p
                     | right _ => poly_symbol l'
                  end
   | nil => default_poly (arity f)

  end.
 
where eq_symb_dec:  forall f g : symbol, {f = g} + {f <> g}
arity : symbol -> nat.
poly: nat -> Set.

I want to define the function poly_cast which a specification is:

poly_cast: forall n m : nat, if n = m then poly n = poly m.

Here is my definition :

Definition poly_cast {n : nat} {m : nat} (x : n = m) :=
     match x with
        | h => poly n = poly m
     end.

I know it is not good function of what I want because when I apply it to the function poly_symbol it gives me an error at : poly_cast h

The term "h" has type "f = g" while it is expected to have type  "?3478 = ?3479".

Could you please give me some suggestion how to build the function poly_cast?
I would like to learn more about how to build a function and dependence type function.

Thank you very much,

Gwen