Changeset 1908 for src/joint/blocks.ma
 Timestamp:
 Apr 26, 2012, 5:38:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/blocks.ma
r1882 r1908 84 84 λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y. 85 85 86 notation > "x ~~> y 'in' c" with precedence 5 1for @{'tunnel_step $c $x $y}.87 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 5 1for @{'tunnel_step $c $x $y}.86 notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}. 87 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}. 88 88 interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y). 89 89 … … 96 96 definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y. 97 97 98 notation > "x ~~>^* y 'in' c" with precedence 5 1for @{'tunnel $c $x $y}.99 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 5 1for @{'tunnel $c $x $y}.98 notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}. 99 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}. 100 100 interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y). 101 101 … … 115 115 ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c. 116 116 117 notation > "x ~~>^+ y 'in' c" with precedence 5 1for @{'tunnel_plus $c $x $y}.118 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 5 1for @{'tunnel_plus $c $x $y}.117 notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}. 118 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}. 119 119 interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y). 120 120 … … 167 167 168 168 169 notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 5 1for169 notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for 170 170 ${default @{'block_in_code $c $b $x $B $y} 171 171 @{'block_in_code $c false $x $B $y} 172 172 }. 173 173 174 notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 5 1for174 notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for 175 175 @{'block_in_code $c $b $x $B $y}. 176 notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 5 1for176 notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for 177 177 @{'block_in_code $c false $x $B $y}. 178 178
Note: See TracChangeset
for help on using the changeset viewer.