Ssreflect Users Discussion List

["Timothy G. Griffin" <>]

Consider the following context: 

Require Import ssreflect ssrbool eqtype seq fintype finfun. 
Variable A : eqType. 
Variable B : eqType. 
Variable  D : finType. 
Variable  f : {ffun D -> prod_eqType A B}. 
Variable p : pred D. 
(* subD is perhaps a clumsy encoding of "{z in Z | p z = true}" *) 
Definition subD : finType := seq_sub_finType (filter p (enum D)). 

Now suppose I want to define a function "g (z : subD) = (f z).1". 
Doing the "obvious" thing does not work: 

Definition g : {ffun subD -> A} := [ffun z => (f z).1]. 

This does not type check: 
   Error: The term "[ffun z => (f z).1]" has type "{ffun D -> A}"
   while it is expected to have type "{ffun subD -> A}".

My question : what is the trick to get this kind of coercion to work? 

thanks,
tim 
http://www.cl.cam.ac.uk/~tgg22/