File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed
source/rust_verify/example/state_machines Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -120,10 +120,10 @@ state_machine!{ TreeSM {
120
120
require let Tree :: Node ( left_child, right_child) = pre. tree;
121
121
if left {
122
122
require let Tree :: Leaf ( old_val_l) = * left_child;
123
- update tree = Tree :: Node ( box Tree :: Leaf ( new_val) , right_child) ;
123
+ update tree = Tree :: Node ( Box :: new ( Tree :: Leaf ( new_val) , right_child) ) ;
124
124
} else {
125
125
require let Tree :: Leaf ( old_val_r) = * right_child;
126
- update tree = Tree :: Node ( left_child, box Tree :: Leaf ( new_val) ) ;
126
+ update tree = Tree :: Node ( left_child, Box :: new ( Tree :: Leaf ( new_val) ) ) ;
127
127
}
128
128
}
129
129
}
@@ -244,13 +244,13 @@ fn take_step(
244
244
lt_leaf_fragment) ;
245
245
let lt2 = LinearTree :: Node (
246
246
lt_root_fragment,
247
- box LinearTree :: Leaf ( lt_leaf_fragment_new) ,
247
+ Box :: new ( LinearTree :: Leaf ( lt_leaf_fragment_new) ) ,
248
248
lt_right
249
249
) ;
250
250
let interp2 = interp;
251
251
let tree2 = TreeSM :: State {
252
252
tree : Tree :: Node (
253
- box Tree :: Leaf ( new_val) ,
253
+ Box :: new ( Tree :: Leaf ( new_val) ) ,
254
254
tree1. get_Node_1 ( )
255
255
)
256
256
} ;
You can’t perform that action at this time.
0 commit comments