The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Fred,

Fred Smith 
<fsmith1024 AT gmail.com>
 writes:

> Emilio,  Although I have played with ssreflect since our last exchange,
> there is obviously much left to learn.  I am glad to see the comprehensive
> support for Fin.t and SubType.

Indeed IMVHO you don't need to use ssreflect at all, but keep in mind
that if you are doing something similar to a "subType", you will end up
replicating much of the existing infrastructure there, which is quite
mature.

> As usual the challenge for me is finding the right term to map to the
> concept I have in mind.

Indeed that's difficult. I don't have so much experience with Coq yet,
but my personal rule of thumb is that the moment I am "having pain" in
my proofs, then I am certainly doing it wrong.

> The jsCoq prototype you linked looks very cool.  Who is doing that
> project?

See: https://github.com/ejgallego/jscoq

Best,
Emilio