[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Tagged formulas

On Friday, January 15, 2016 at 10:31:22 AM UTC+2, Ron Pressler wrote:
For completeness, here's my new spec:

    * The priming operator is defined thus: e' == e with all its variables primed, except those enclosed in a CAPTURE block.

    *  It is level-incorrect to write CAPTURE e, if e does not have level at most 1

    *  When appearing in an unprimed _expression_, CAPTURE e has the same meaning as e.

The spec does not define the syntactic scope (precedence) of CAPTURE, but that is orthogonal. Perhaps it would be better to use some symbol or a special bracketing to delimit the captured _expression_, rather than use the word CAPTURE, which seems like an operator.

BTW, the restriction of CAPTURE to level <= 1 expressions comes naturally from CAPTURE being defined in terms of prime and vice-versa: You can only capture expressions that you can prime (and vice-versa).