Ssreflect Users Discussion List

[Georges Gonthier <>]

  You are probably right, we could use D : pred aT; it's likely the case that 
the declaration dates back to an early version of finset where the second
argument of imset was restricted to a {set _}.
  One disadvantage of this declaration, though, is that it makes it difficult 
to provide D as an explicit arguments to, say, eq_imset, because {set _}s are 
not allowed to coerce  (pred _). This is a general issue in both fintype and 
finset. The solution would be to use pred_class (defined in ssrbool.v) rather 
than pred as the type of generic predicates (or rather, a variant of 
pred_class that allows specifying the domain type), but that's a somewhat 
larger refactoring job.

   Georegs

-----Original Message-----
From: Cyril Cohen [] 
Sent: 05 July 2013 13:03
To: 
Subject: Changing {set aT} to (pred aT) in eq_imset?

Hi,

Would you mind if I changed it, or is there a reason for D being a {set aT} 
instead of a (pred aT) in the implicit types declaration line 1325 of 
finset.v?

It seems that the version where D is a (pred aT) would be more general, 
compatible with the definition of pcycles (in perm.v) and moreover it still 
makes the full FT proof compile.

Cheers,
--
Cyril