Phil,
On 5 Jun 2011, at 22:53, Phil Clayton wrote:
> I've noticed that the ProofPower-Z grammar accepts lambda expressions without
> a spot, e.g.
>
> (%lambda% x : X)
>
> because it uses the same grammar rules as for mu expressions. Such
> expressions always produce the error message
>
> E
Phil,
On 5 Jun 2011, at 12:10, Phil Clayton wrote:
> (Examples also included in attached file char_tuple_issue.sml)
>
> After defining e.g.
>
> [T]
>
> S %def% [X : T]
>
> the type inference issue with characteristic tuples can be seen when the term
>
> {S; S'}
>
> occurs as a subterm.
Rob Arthan wrote:
On 5 Jun 2011, at 12:10, Phil Clayton wrote:
I suppose this is a good opportunity to raise item 219, i.e.
1. Should the Spivey-Z schema decoration S' be supported in
ProofPower-Z? I believe Standard-Z requires one of
(S)'
S '
to decorate a schema reference S. This avo
