[CST-2] Types: Ex 4.3.2

[Steve Bishop]

> > let x = ((\x.x) (\x.x)) in (x 5)
> > 
> > Since A != {} and M1 is an application...
> 
> That's what I thought originally but I guess it
> depends on whether you do the Beta reduction
> before *or* after the assignment to x.

Surely you don't do any reductions (which are equivalent to evaluation)
before you type it!?

-- 
Steve Bishop
President - Cambridge University Caving Club - http://cucc.survex.com/

smb50@cam.ac.uk - http://smb50.quns.cam.ac.uk/ - Mobile 07748 960856
Queens' College, Cambridge. CB3 9ET