The Coq mailing list

[Satrajit Roy <admin AT satrajit.com>]

Hi guys!!!!
I have been grappling with polymorphism in Coq for a while. So thought a concrete example might make it easier for people to answer.

Let's say I have:

Inductive policy_kind:Set :=
    policy_a | policy_b.

Record policy_A:Set := A {a_def : bool, a_cur:bool}.
Record policy_b:Set := B {b_def: nat, b_max:nat,b_cur:nat}.

What should be the correct definition for 'policy' if I want to do something like the following:

Definition policy (k:policy_kind) (data:list <?>) : <?> :=
    match k with
       | policy_a => A (nth 0 data) (nth 1 data) (*nth must return a bool*)
       | policy_b => B (nth 0 data) (nth 1 data) (nth 2 data) (*nth must return a nat*)
end.

I know I can do it differently, but I want to do it this way so that the accessor functions are auto generated.

There may be syntax errors
 in the above, but, basically I need to figure out what would the terms be that should replace the '?" in the above definition.

Thanks in anticipation.