Dear Ramana,
Indeed, this is apparently missing in lib/coq/set/Fset.v.
Here it is:
Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType
(fset a).
Proof.
intros.
split.
exists (fun _ => false).
exists nil. split; [ apply List.NoDup_nil | intuition; discriminate H ].
intros x y.
Dear Why3-club,
I'm working on a development that uses the Fset's module extensively and
would like to use Coq to prove a few goals. I notice there is no
WhyType instance for Fset.fset. While it is fairly straightforward to
derive one, it can get cumbersome to have to do so for each goal
On Wed, 30 Jan 2019, François Bobot wrote:
> Le 30/01/2019 à 13:36, Julia Lawall a écrit :
> > I have the following orgnization of modules:
> >
> > A parameterized by f
> >
> > B uses A
> >
> > C uses A and B and is parameterized by g
> >
> > D uses A, B and C and provides a definition for f
Le 30/01/2019 à 13:36, Julia Lawall a écrit :
> I have the following orgnization of modules:
>
> A parameterized by f
>
> B uses A
>
> C uses A and B and is parameterized by g
>
> D uses A, B and C and provides a definition for f and for g
> The definition for g relies on things defined in A
Hello,
I have the following orgnization of modules:
A parameterized by f
B uses A
C uses A and B and is parameterized by g
D uses A, B and C and provides a definition for f and for g
The definition for g relies on things defined in A and B.
How can I set this up? In D, I cannot just clone
