1. Generic global variablesUnder certain conditions, strokes in the names of generic global variables (other than %bbU%) are not printed. (In particular, this affects generic global variables that are not "template forms with one or more non-%bbU% generic actual parameters".)
In imp064, function do_generic, I believe references to 'name' on lines 1350 and 1353 should refer to 'fullname'. That change fixes most of the test failures.
2. Decorated global variable name clashWhen both C and C' are schema references, (C)' is printed as C' which is a different term.
In imp064, the problem appears to be in function do_decor. There appear to be two routes to fixing this:
A. Print in Spivey-Z with minimal parentheses, using the current theory to determine whether parentheses are necessary, i.e. print C' for (C)' if C' is not the name of a global variable.
B. Print in Standard-Z by always using enclosing parentheses for decoration, i.e. print (C)' even if it is valid to print C'.
I think B can be achieved by simply dropping the ZLVar and ZGVar cases on lines 670 and 671 of imp064.
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com