Problem with instantiation of interfaces
Consider the following piece of WhyML code:
module M
type t 'a = 'a -> int
end
module N : M
end
Let us assume this is the contents of a foo.mlw
file. If we use why3 prove foo.mlw
, then Why3 replies with the error
Symbol t not found in implementation
However, if we change module N into
module N : M
type t 'a = 'a -> int
end
then we get the error
Cannot instantiate a defined symbol t