I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-
> 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
