[Why3-club] WhyML questions: function without body? polymorphic Sum?

David MENTRE dmentre at linux-france.org
Wed Nov 28 08:35:45 CET 2012


Hello Guillaume,

2012/11/27 Guillaume Melquiond <guillaume.melquiond at inria.fr>:
> I had a discussion with Andrei about it and it appears that, while there
> are no theoretical difficulties with such a feature, there are several
> technical ones, so it might not happen anytime soon.

OK, thank you for taking a look at it. I am currently trying to
formalize small parts of a Real World(tm) specification using Why3 and
polymorphic data type seemed really suited for some parts. But right
now I am not fully sure it is really needed in practice, i.e. it is
the right way to formalize it. I'll let you know if I have a real use
case for it.

Anyway, I can always work around this issue by using the old
copy/paste approach. ;-)

Best regards,
david



More information about the Why3-club mailing list