Hello Claude,
Le 16/11/2016 à 10:08, Claude Marché a écrit :
> assert { A by B so C }
>
> then after using "split" you will have to prove :
>
> . B
> . B -> C
> . B /\ C -> A
>
> but more importantly, in the code after the assert, the only visible
> extra hypothesis will be A. B and C will not be visible.
>
> This addition of "by" and "so" is a lightweight technique to allow local
> additional hints, and more generally provides some simple form of
> declarative proof.
Thank you, the explanation is clear.
Best regards,
david
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
