From 9eabd7da37d55b049cbff4d9aacec1758e00167e Mon Sep 17 00:00:00 2001 From: mehbark Date: Wed, 9 Apr 2025 16:02:04 -0400 Subject: [PATCH] `Ast.run_compiled` --- Bytecode/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) 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)