[CST-2] Strictness 99.8.7

[Phebe Mann]

Moritz

 |' = capital gamma symbol,
 --> (S) = an arrow with an S floating above it]
 --> (S') = an arrow with an S' floating above it]
(SUB rule)
   |' |- f : int^k  -->(S') int
-----------------------------
   |' |- f : int^k  --> (S) int
where S' is a subset of S

k = no. of parameter
S = set of parameters that are guaranteed to loop

Phebe

On Fri, 1 Jun 2001, M.Y.W.Y. Becker wrote:

>
>
> --On 01 June 2001 17:03 +0100 Phebe Mann <pm258@hermes.cam.ac.uk> wrote:
> [...]
> > (SUB rule)
> >    |' |- f : int^k  --> (S) int   if S' is a subset of S
> > -----------------------------
> >    |' |- f : int^k  --> (S') int
> > where S' is a subset of S
> [...]
>
> That's wrong. Raymond's answer was already 100% correct (I believe).
>
> Mo
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>