coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Set and heterogeneous lists

From: Adam Chlipala <adam AT chlipala.net>
To: Christian Doczkal <doczkal AT ps.uni-sb.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Set and heterogeneous lists
Date: Fri, 12 Mar 2010 09:40:39 -0500

Christian Doczkal wrote:

Variable Ts : list Tp.
Check (list Tp). (* Set *)
Check (hlist (map Tm Ts)).
(* fails: The term "map Tm Ts" has type "list Set"
while it is expected to have type "list Type". *)

A simple type annotation fixes this:
Check (hlist (map (B := Type) Tm Ts)).

[Coq-Club] Set and heterogeneous lists, Christian Doczkal
- Re: [Coq-Club] Set and heterogeneous lists, Adam Chlipala