On 23 Apr 2012, at 17:33, Roger Bishop Jones wrote:
> Rob was rather definite in his rejection of my "prohibition"
> interpretation (of Spivey) without saying why.
>
Perhaps I hit send to soon. I was using what fuzz does as an indicator of Mike
Spivey's intentions. fuzz accepts the following:
On Friday 20 Apr 2012 13:36, Steve King wrote:
> For interest, my recollection is that the Standard's
> definition of variable scope was based on:
> - the idea of a *set* of a declarations: decl1; decl2
> should have 'the same effect' as decl2; decl1.
This is in "Understanding Z" though its not cl
On 20/04/12 18:48, Phil Clayton wrote:
On 20/04/12 11:19, Rob Arthan wrote:
...
A == 1 .. 10
S ^= [A : A x A | (_+_)A< 10]
...
And as so often, language decisions that are bad for proof are often
bad for pedagogical and other reasons too. In this case, it stops the
language being closed und
On 20/04/12 11:19, Rob Arthan wrote:
...
A == 1 .. 10
S ^= [A : A x A | (_+_)A< 10]
...
And as so often, language decisions that are bad for proof are often bad for
pedagogical and other reasons too. In this case, it stops the language being
closed under certain desirable transformations.
Roger,
Thanks for the background and explanation. I have added responses below.
On 15/04/12 15:21, Roger Bishop Jones wrote:
Thanks for your comments on the ProofPower-Z scope rules
Phil.
I personally believe that the ProofPower position on the
scope of variables is preferable to "the" alter
On 15 Apr 2012, at 15:21, Roger Bishop Jones wrote:
> Thanks for your comments on the ProofPower-Z scope rules
> Phil.
>
> I personally believe that the ProofPower position on the
> scope of variables is preferable to "the" alternative, for
> reasons I will come to shortly, but I think it pos
Thanks for your comments on the ProofPower-Z scope rules
Phil.
I personally believe that the ProofPower position on the
scope of variables is preferable to "the" alternative, for
reasons I will come to shortly, but I think it possible that
in coming to the decision I was partly influenced by a
In ProofPower-Z, the scope of a variable declared in the Decl part of a
SchemaText includes all expressions in the Decl, for example, in
x : E1; y : E2
any free occurrence of x or y in E1 or E2 is the bound x or y.
I recently got caught out by a subtle case whilst systematically
constructin
