mbk/bytecode
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Ast.run_compiled

Browse source
This commit is contained in:
mehbark 2025-04-09 16:02:04 -04:00
parent 191c09ace7
commit 9eabd7da37
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
Bytecode/Basic.lean
View file

@ -78,3 +78,8 @@ theorem Ast.compile_eq_push_interpret (ast : Ast)
theorem Ast.compile_sound (ast : Ast) theorem Ast.compile_sound (ast : Ast)
: ast.compile.run = ast.interpret := by : ast.compile.run = ast.interpret := by
simp [M.run, compile_eq_push_interpret, M.push_pop, pure, OptionT.pure, StateT.pure] 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)