Ssreflect Users Discussion List

[Pierre-Yves Strub <>]

Hi,

This might solve your problem:

https://github.com/math-comp/finmap

Best. Pierre-Yves.

2017-11-22 6:04 GMT+01:00 Abhishek Kr Singh 
<>:
> Hi,
>
> I am working on the formalisation of some results on finite structures
> (graphs and posets). I was trying to explore the possibility of using
> ssreflect library.
> All the structures which I want to talk about in the proofs are finite.
> However, in the very beginning I cannot assume the elements of my sets from
> finType.
> For example, I want to start reasoning with a finite simple graph where in
> the middle of the proof the nodes of the graphs are replaced with cliques of
> different sizes. Therefore the finite set type from ssreflect seems to be a
> little more restrictive. I cannot assume in the beginning all the vertices
> of the graph are from some finType.
>  Is there some work which builds a finite set  library (common results on
> finite sets) starting from the countable type in ssreflect ?
>
>
> --
> Thanks and Regards.
>
> Abhishek Kr. Singh,
> Research Scholar, STCS, TIFR Mumbai.
> Homepage:  http://www.tcs.tifr.res.in/~abhishek/
>
>  http://www.tcs.tifr.res.in/people/abhishek-singh
>