Changes between Version 12 and Version 13 of PrefixMinusResolution


Ignore:
Timestamp:
Jul 15, 2010 7:59:16 AM (4 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.)