Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-02 20:54:07 -0800 (Sat, 02 Apr 2005)
Revision: 7092
Log message:
This augments the basic term type, adding support for the "shape" parameters.
Syntax:
- write "operator[op:sh]" for the shape meta-parameter "op"
- write "opetator[('t1 't2)]" or opetator[('t1 't2):sh] for a concrete shape
"apply[]{0; 0}"
TODO:
- Add support for display forms (add slot[s:sh]; make sure that in the "src"
mode shapes are printed in a parseable way)
- Convert the reflection theory to using the shape parameters in operators.
WARNING: This breaks backwards compatibility for binary files. Export your
proofs before updating.