ge --
From: "Claude Marché"
To: "why3-club@lists.gforge.inria.fr"
Sent: 01/02/2018 16:45:49
Subject: Re: [Why3-club] Tuples and counter-examples printing
>
>Hello Denis,
>
>As far as I know, the decomposition of the quantifications over tuples
>is done
Hello Denis,
As far as I know, the decomposition of the quantifications over tuples
is done quite early in the Why3 processing ("eval_match" in the WP calculus)
Using a record structure is probably a good workaround, and I don't
think you need to bother with any "model_projection" labels for tha
Dear list,
I'm stucked with an apparently simple problem of counter-examples printing and
I'd appreciate a lot if someone had a clue to help me.
I have a Why3 formalization that deals with Bool tuples. And I'd like to print
those tuples values when a counter-example is found.
Here's an example:
