On Thu, 21 Feb 2019, Jean-Jacques Levy wrote:
> I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-
I'll look into that, thanks.
julia
>
> > Le 21 févr. 2019 à 16:46, Julia Lawall <julia.law...@lip6.fr> a écrit :
> >
> >
> >
> > On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:
> >
> >>
> >> Hello,
> >>
> >> Use the keyword `by`:
> >>
> >> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x =
> >> Array.make 1 1 }
> >
> > Is by useful for anything else? Sometimes I know that a particular lemma
> > should be useful for proving something, and from the English meaning of
> > "by" it would be nice to be able to say by useful_lemma. But that doesn't
> > work.
> >
> > julia
> >
> >>
> >> Raphaël
> >>
> >> On 21/02/2019 15:47, Alan Schmitt wrote:
> >> Hello,
> >>
> >> I have this very simple specification that creates a type and
> >> states an
> >> invariant for it.
> >>
> >> module Test
> >>
> >> use int.Int
> >> use array.Array
> >>
> >> type t = { x : array int }
> >> invariant { length x > 0 /\ x[0] > 0 }
> >>
> >> end
> >>
> >> When I load this in why3, I'm asked to check that the type is
> >> inhabited.
> >> Is there a way to provide a witness, as why3 is unable to guess
> >> it?
> >>
> >> Thanks,
> >>
> >> Alan
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >>
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
