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

un-only M.push_pop closing simp

Browse source
This commit is contained in:
mehbark 2025-04-11 18:18:24 -04:00
parent 9eabd7da37
commit 46d44e4e49
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Bytecode/Basic.lean
View file

@ -62,9 +62,9 @@ def M.run (m : M Unit) : Option Rat :=
theorem M.push_pop : (do push x; pop) = pure x := by
funext xs
-- what on earth
simp only [bind, OptionT.bind, OptionT.mk, StateT.bind, push, modify, modifyGet,
simp [bind, OptionT.bind, OptionT.mk, StateT.bind, push, modify, modifyGet,
MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, OptionT.lift, StateT.modifyGet, pure,
StateT.pure, pop, getModify, Array.pop_push, Array.back?_push, OptionT.pure]
StateT.pure, pop, getModify, OptionT.pure]
theorem Ast.compile_eq_push_interpret (ast : Ast)
: ast.compile = M.push ast.interpret := by