[Why3-club] Coq driver
guillaume.melquiond at inria.fr
Tue Mar 18 06:17:38 CET 2014
On 18/03/2014 02:49, Jean-Jacques Levy wrote:
> 2- I do not get the point [you meant that you cannot use a type previously defined in a new one ??!!]. But now it works.
No, it is a bit more complicated; it happens when the definition of an
inductive type crosses another inductive type. (Otherwise we would
hopefully have encountered the bug much earlier.)
When you have "type t 'a = ...", the corresponding Coq inductive type
requires a proof that 'a is not empty. So, when you have "type u = ...
(t u)", Coq asks you to build a proof that u is not empty. But since you
are in the process of defining u, you cannot prove yet that it is not
empty. Hence the bug you encountered.
A possible fix is to move the type constraints from the polymorphic type
definitions to the polymorphic function definitions. That would fix the
issue above, but I don't know yet if that won't break something else.
More information about the Why3-club