search

math-comp / finmap

Finite sets, finite maps, multisets and generic sets
46 stars 28 forks source link

Missing coercion from finSet to finType #102

Open rhz opened 1 year ago

rhz commented 1 year ago

It'd be nice if fset_sub_finType would be made a coercion.

Coercion fset_sub_finType : finSet >-> finType.