Hi,
The standard library contains a file named function.mlw, but its use
as in the following example gives a syntax error, because 'function' is
a keyword of WhyML.
module Inverses
type t
type u
function t2u t : u
function u2t u : t
clone function.Bijective with type a = t, type v = u,
function to_ = t2u, function from = u2t, axiom Inj
end
Is there another way to use this file?
Best regards,
Alain
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
