Changeset 1908


Ignore:
Timestamp:
Apr 26, 2012, 5:38:07 PM (7 years ago)
Author:
fguidi
Message:

notation fixup following last commit of matita
we shifted the levels of precedence from 50 to 60 up by 5

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1882 r1908  
    739739   
    740740notation "hvbox(a break ⊎ b)"
    741  left associative with precedence 50
     741 left associative with precedence 55
    742742for @{ 'disjoint_union $a $b }.
    743743interpretation "sum" 'disjoint_union A B = (Sum A B).
  • src/ASM/Vector.ma

    r1646 r1908  
    2727
    2828notation "hvbox(hd break ::: tl)"
    29   right associative with precedence 52
     29  right associative with precedence 57
    3030  for @{ 'vcons $hd $tl }.
    3131
  • src/common/Identifiers.ma

    r1882 r1908  
    401401    (match s' with [ an_id_map s1 ⇒ s1 ])).
    402402
    403 notation "a ∖ b" left associative with precedence 50 for @{'setminus $a $b}.
     403notation "a ∖ b" left associative with precedence 55 for @{'setminus $a $b}.
    404404
    405405interpretation "identifier set union" 'union a b = (union_set ??? a b).
  • src/joint/Joint_paolo.ma

    r1882 r1908  
    7474  | extension: ext_step p → joint_step p globals.
    7575
    76 notation "r ← a1 .op. a2" with precedence 55 for
     76notation "r ← a1 .op. a2" with precedence 60 for
    7777  @{'op2 $op $r $a1 $a2}.
    78 notation "r ← . op . a" with precedence 55 for
     78notation "r ← . op . a" with precedence 60 for
    7979  @{'op1 $op $r $a}.
    80 notation "r ← a" with precedence 55 for
     80notation "r ← a" with precedence 60 for
    8181  @{'mov $r $a}. (* to be set in individual languages *)
    82 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     82notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
    8383  @{'opaccs $op $r $s $a1 $a2}.
    8484
  • src/joint/blocks.ma

    r1882 r1908  
    8484  λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y.
    8585
    86 notation > "x ~~> y 'in' c" with precedence 51 for @{'tunnel_step $c $x $y}.
    87 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel_step $c $x $y}.
     86notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}.
     87notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}.
    8888interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y).
    8989
     
    9696definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y.
    9797
    98 notation > "x ~~>^* y 'in' c" with precedence 51 for @{'tunnel $c $x $y}.
    99 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel $c $x $y}.
     98notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}.
     99notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}.
    100100interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y).
    101101
     
    115115  ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c.
    116116
    117 notation > "x ~~>^+ y 'in' c" with precedence 51 for @{'tunnel_plus $c $x $y}.
    118 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel_plus $c $x $y}.
     117notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}.
     118notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}.
    119119interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y).
    120120
     
    167167   
    168168
    169 notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 51 for
     169notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for
    170170  ${default @{'block_in_code $c $b $x $B $y}
    171171            @{'block_in_code $c false $x $B $y}
    172172  }.
    173173 
    174 notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 51 for
     174notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    175175  @{'block_in_code $c $b $x $B $y}.
    176 notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 51 for
     176notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    177177  @{'block_in_code $c false $x $B $y}.
    178178
  • src/utilities/proper.ma

    r1640 r1908  
    1313interpretation "proper contravariant" 'proper_contra r s = (proper_contra ? ? r s).
    1414
    15 notation "r ++> s" right associative with precedence 51 for
     15notation "r ++> s" right associative with precedence 56 for
    1616  @{'proper $r $s}.
    1717
    18 notation "r -+> s" right associative with precedence 51 for
     18notation "r -+> s" right associative with precedence 56 for
    1919  @{'proper_contra $r $s}.
    2020
    2121(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
    22 notation > "f ⊨ p " with precedence 50 for @{$p $f $f}.
     22notation > "f ⊨ p " with precedence 55 for @{$p $f $f}.
Note: See TracChangeset for help on using the changeset viewer.