Changes between Version 12 and Version 13 of PrefixMinusResolution


Ignore:
Timestamp:
Jul 15, 2010 7:59:16 AM (5 years ago)
Author:
maeder
Comment:

added compromise

Legend:

Unmodified
Added
Removed
Modified
  • PrefixMinusResolution

    v12 v13  
    7171
    7272x8 will be resolved as "(- 4) # (5 # 6)" like it would for any right-associative operator # with lower precedence, too. For any
    73 ''non-associative'' operator # "- 4 # 5 # 6" is rejected like "4 # 5 # 6" or "-(4 # 5 # 6)" would be.
     73''non-associative'' operator # "- 4 # 5 # 6" is rejected like "4 # 5 # 6", "-(4 # 5 # 6)" or "(-4) # 5 # 6" would be.
    7474
    7575Surely, one can always disallow "confusing" resolutions, but if we reject "- 4 # 5", we can also reject "- 4 - 5" or "`- 4 ^ 5`".
     
    125125
    126126This (surprisingly) makes "{{{- a `f` b}}}" resolve as "{{{- (a `f` b)}}}" for any f without fixity declaration (independent of this proposal). This contradicts NegationBindsTightly.
     127
     128But as a compromise it is also an option to simple reject terms where prefix minus would not bind tightly (enough), which makes sense for `-a ^ b` and would force us to write `-(a ^ b)` or `(-a) ^ b` explicitly. (Of course one would not want to reject "-a * b", no matter how it is resolved.)