Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 17:14:46 -0800 (Sat, 05 Feb 2005)
Revision: 6603
Log message:
Added display-form type checking. This was a little painful because
some theories were using xlist as a normal list. In the end, I changed
the declarations to the following.
declare xcons{'a : Dform; 'b : Dform} : Dform
declare xnil : Dform
Base_reflection has its own list, using rcons and rnil.
You need to use the functions mk_rlist_term, is_rlist_term, etc.,
instead of mk_xlist_term, is_xlist_term.
The .prla updates are just for the opname renaming.