From your answers, I now understand that 'export' and 'as' control the
names of objects, not their visibility, as I initially thought. Thanks.
Le 25/09/2020 à 19:42, Guillaume Melquiond a écrit :
Le 25/09/2020 à 19:17, Alain Giorgetti a écrit :
In the following example, an error 'unbound prop
Le 25/09/2020 à 19:17, Alain Giorgetti a écrit :
> In the following example, an error 'unbound proposition symbol' Inj ''
> is reported for M2. It is as if the presence of 'as' forced the export.
> Is it wanted and written somewhere?
>
> module MwithAs
> clone "function".Injective as I with axi
Thanks for your answers. My question was mainly on the semantics of 'as'.
In the following example, an error 'unbound proposition symbol' Inj ''
is reported for M2. It is as if the presence of 'as' forced the export.
Is it wanted and written somewhere?
module MwithAs
clone "function".Inject
Le 25/09/2020 à 09:30, Claude Marche a écrit :
>> Since lemmas cannot be referred to, this indeed
>> seems like an artificial limitation
> .
> Not true : you can do "apply H", "rewrite H" and these kinds of things
> in the interactive theorem proving interface of Why3, without forgetting
> the sim
Le 23/09/2020 à 14:36, Guillaume Melquiond a écrit :
Since lemmas cannot be referred to, this indeed
seems like an artificial limitation
.
Not true : you can do "apply H", "rewrite H" and these kinds of things
in the interactive theorem proving interface of Why3, without forgetting
the simil
Hello,
On Tue, 22 Sep 2020 at 13:46, wrote:
> Dear All,
>
> Thanks Andrei for the answer.
>
> There is another issue that refrains me to propose a review of this file:
>
> Assuming that the goals in it are replaced by lemmas, we would like the
> Bijective
> module to export all the lemmas of the
Le 22/09/2020 à 13:45, alain.giorge...@femto-st.fr a écrit :
> Assuming that the goals in it are replaced by lemmas, we would like the
> Bijective module to export all the lemmas of the Injective and Surjective
> modules
> it clones. But these lemmas have the same name, and 'export' and 'as XX' a
Dear All,
Thanks Andrei for the answer.
There is another issue that refrains me to propose a review of this file:
Assuming that the goals in it are replaced by lemmas, we would like the
Bijective
module to export all the lemmas of the Injective and Surjective modules
it clones. But
these lemm
Hi Alain,
there is indeed a way of using files with strange names that are not valid
WhyML identifiers: just put the name of the file in double quotes like a
string constant:
clone "function".Bijective with ...
That said, I don't think it's reasonable to have such files in our standard
library,
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 =
10 matches
Mail list logo
