[@inline:trivial] on the definition of a predicate is useful because it
allows proofs to directly use the definition of the predicate. But it
seems to also make it hard to prove that a use of a predicate follows from
itself. Eg if pred has this annotation, then having
pred a b c d
as a hypothes
Jean-Christophe
On 7/13/19 3:03 PM, Julia Lawall wrote:
>
>
> On Sat, 13 Jul 2019, Jean-Christophe Filliatre wrote:
>
>> Hi Julia,
>>
>> Indeed it is. The syntax is
>>
>> apply Lemma with term1,term2,...,termk
>>
>> For instance, in the following situation
>>
>> lemma L: forall x y z. p x
On Sat, 13 Jul 2019, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> Indeed it is. The syntax is
>
> apply Lemma with term1,term2,...,termk
>
> For instance, in the following situation
>
> lemma L: forall x y z. p x -> p z -> p y
> goal G: p 42
>
> you can do
>
> apply L with 21,21
>
>
On Sat, 13 Jul 2019, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> Indeed it is. The syntax is
>
> apply Lemma with term1,term2,...,termk
>
> For instance, in the following situation
>
> lemma L: forall x y z. p x -> p z -> p y
> goal G: p 42
>
> you can do
>
> apply L with 21,21
>
>
Hi Julia,
Indeed it is. The syntax is
apply Lemma with term1,term2,...,termk
For instance, in the following situation
lemma L: forall x y z. p x -> p z -> p y
goal G: p 42
you can do
apply L with 21,21
Then the value for "y" (42) is inferred when matching the goal and the
lemma's con
I guess the apply transformation is a way to force a lemma to be used at a
particular place in a proof? How does one specify the list of arguments,
ie a value of list term type?
thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
ht
