Notation question

[Mark Carroll]

On Mon, 28 May 2001, Juan Carlos Arevalo Baeza wrote:

> 
>     Just a very naive question, because I'm really curious. I've seen in 
> previous messages here discussions about type systems using this kind of 
> notation:
> 
> >  G |- f :: all x::S . T   G |- s :: S
> >--------------------------------------
> >          G |- f s :: [s/x]T
> 
>     I'd never seen it before, and a few searches I've launched over the net 
> have turned up just a couple more examples of this notation, but without a 
> single reference to how it works or what it means, or even what it's 
> called, for that matter.
> 
>    I'd appreciate any pointers.
(snip)

I'm far from the right person to have a go, but while we're waiting for
someone who knows what they're talking about:

I bet that |- is 'entails'. My impression of it is rather like 'implies',
but clearly that's not quite right or we wouldn't need a different term
for it.

The . might be 'such that'.

The thing below the ----- might be a consequence of the two things above
it.

The [s/x]T means, probably, "T with s substituted for any occurrence of
x". (Did I get that the right way around?)

I hope that's a start.

-- Mark