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

chore: cleanup

Browse source
This commit is contained in:
mehbark 2025-04-09 15:56:50 -04:00
parent 9fabb90680
commit 191c09ace7
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Bytecode/Basic.lean
View file

@ -44,7 +44,6 @@ abbrev M.op (l r : M Unit) (f : Rat → Rat → Rat) : M Unit := do
let r ← pop let r ← pop
push (f l r) push (f l r)
def Ast.compile : Ast → M Unit def Ast.compile : Ast → M Unit
| lit n => M.push n | lit n => M.push n
| add l r => M.op l.compile r.compile (·+·) | add l r => M.op l.compile r.compile (·+·)
@ -67,11 +66,6 @@ theorem M.push_pop : (do push x; pop) = pure x := by
MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, OptionT.lift, StateT.modifyGet, pure, 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, Array.pop_push, Array.back?_push, OptionT.pure]
-- instance : LawfulMonad M where
-- map_const := rfl
-- id_map {a} x := by
-- simp [Functor.map, OptionT.bind, OptionT.mk, StateT.instLawfulMonad]
theorem Ast.compile_eq_push_interpret (ast : Ast) theorem Ast.compile_eq_push_interpret (ast : Ast)
: ast.compile = M.push ast.interpret := by : ast.compile = M.push ast.interpret := by
induction ast induction ast