Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 14:20:12 -0800 (Mon, 09 Jan 2006)
Revision: 8434
Log message:
Investigate a new plan of attack, where we prove theorems for all the
common cases, say for mk_bterm up to arity 5.
Place all the common cases in a "naive" BTerm normalizer, and run
it before the general normalizer.
This will continue to work, because it falls back to the general
normalizer, but it should be faster if we have theorems for the common
cases.
Changes | Path |
+83 -2 | metaprl/theories/itt/reflection/experimental/itt_hoas_normalize.ml |
+4848 -876 | metaprl/theories/itt/reflection/experimental/itt_hoas_normalize.prla |