The Coq mailing list

[Takashi MIYAMOTO <tmiya AT bu.iij4u.or.jp>]

Dear all,

I am trying to write a mapping function from a list of Z to a list of subset 
type ZH.
The definition of function ZHs_of_Zs fails. It seems that my usage of refine 
tactic is wrong.
Could you give an advice how to write functions like this?

---

Require Import ZArith.
Parameter Max:Z.
Parameter HMax:(Max >= 2)%Z.
Definition ZH := {z:Z | (0<=z<Max)%Z}.

Definition ZHs_of_Zs(zs:list Z)(H:forall z, In z zs -> (0<=z<Max)%Z) :list ZH.
refine (fix f (zs:list Z)(_:forall z, In z zs -> (0<=z<Max)%Z):list ZH :=
  match zs return (list ZH) with
  | nil => nil
  | z::zs' => {z|_} :: (f zs' _)
  end).

---

Thank you in advance.

===================================
Takashi Miyamoto