Skip to content

Commit

Permalink
refactor: fix indentation
Browse files Browse the repository at this point in the history
  • Loading branch information
0xMushow committed Nov 13, 2024
1 parent 6004d2f commit 0776891
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
Original file line number Diff line number Diff line change
Expand Up @@ -1080,12 +1080,12 @@ Definition execute_instruction (pc : Z)
}
*)
| Bytecode.WriteRef =>
letS!? reference := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_operand_stack $ Stack.Impl_Stack.pop_as Reference.t) in
letS!? value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_operand_stack Stack.Impl_Stack.pop) in
letS!? _ := returnS! $ Impl_ReferenceImpl.write_ref reference value in
returnS! $ Result.Ok InstrRet.Ok
letS!? reference := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_operand_stack $ Stack.Impl_Stack.pop_as Reference.t) in
letS!? value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_operand_stack Stack.Impl_Stack.pop) in
letS!? _ := returnS! $ Impl_ReferenceImpl.write_ref reference value in
returnS! $ Result.Ok InstrRet.Ok

(*
Bytecode::CastU8 => {
Expand Down

0 comments on commit 0776891

Please sign in to comment.