Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 11:08:01 -0800 (Thu, 03 Feb 2005)
Revision: 6582
Log message:
Ported the display form changes, and removed the wildcard types
for unknown terms.
Added types for quoted terms. For example if we have
declare lambda{x : T1. 'e['x] : T2} : T3
then we also get
lambda[@]{x : Term. Term} : Term
I would rather use a type Quote for quoted terms, but this will
surely break in ITT. For example, the following would be
well-typed:
apply[@]{t1[@]; t2[@]}
but the following would break
apply[@]{fst{pair{t1[@]; t0[@]}}; t2[@]}