diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean
index b1fc9bb..2b6aa4f 100644
--- a/Bytecode/Basic.lean
+++ b/Bytecode/Basic.lean
@@ -78,3 +78,8 @@ theorem Ast.compile_eq_push_interpret (ast : Ast)
 theorem Ast.compile_sound (ast : Ast)
     : ast.compile.run = ast.interpret := by
   simp [M.run, compile_eq_push_interpret, M.push_pop, pure, OptionT.pure, StateT.pure]
+
+def Ast.run_compiled (ast : Ast) : Rat :=
+  ast.compile.run.get (by simp [Ast.compile_sound])
+
+#eval Ast.run_compiled (3/2 + 0.5)