# Changeset 1908 for src/joint/blocks.ma

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

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

File:
1 edited

Unmodified
Added
Removed
• ## src/joint/blocks.ma

 r1882 λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y. notation > "x ~~> y 'in' c" with precedence 51 for @{'tunnel_step \$c \$x \$y}. notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel_step \$c \$x \$y}. notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step \$c \$x \$y}. notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step \$c \$x \$y}. interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y). definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y. notation > "x ~~>^* y 'in' c" with precedence 51 for @{'tunnel \$c \$x \$y}. notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel \$c \$x \$y}. notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel \$c \$x \$y}. notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel \$c \$x \$y}. interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y). ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c. notation > "x ~~>^+ y 'in' c" with precedence 51 for @{'tunnel_plus \$c \$x \$y}. notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 51 for @{'tunnel_plus \$c \$x \$y}. notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus \$c \$x \$y}. notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus \$c \$x \$y}. interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y). notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 51 for notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for \${default @{'block_in_code \$c \$b \$x \$B \$y} @{'block_in_code \$c false \$x \$B \$y} }. notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 51 for notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'block_in_code \$c \$b \$x \$B \$y}. notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 51 for notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'block_in_code \$c false \$x \$B \$y}.
Note: See TracChangeset for help on using the changeset viewer.