John Hughes said
G |- f :: all x::S . T G |- s :: S -------------------------------------- G |- f s :: [s/x]T
Any more takers? I still don't have any pointers to literature where this theorem notation is explained more fully, and I'd really like to have some.
This is a standard notation for describing type systems in articles on the subject -- so standard that it's hard to think of a good reference that actually explains it!
and not just type systems but also other aspects of operational semantics. What we have here is a single rule from a rule-based inductive definition of a certain relation G |- s :: S between typing environments G, expressions s and types S. I seem to spend half my life using such inductive definitions and the other half teaching them to undergraduates (and the third half doing university administration, hey ho). Casting modesty aside, to read about such things let me recommend <www.cl.cam.ac.uk/Teaching/2000/Semantics/> lecture notes on operational semantics (esp section 2.3) Andy Pitts