Changeset 1908 for src/joint


Ignore:
Timestamp:
Apr 26, 2012, 5:38:07 PM (8 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/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.