From 191c09ace7805f429dd8116059390b51555f1b88 Mon Sep 17 00:00:00 2001 From: mehbark Date: Wed, 9 Apr 2025 15:56:50 -0400 Subject: [PATCH] chore: cleanup --- Bytecode/Basic.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean index 6e6db8f..b1fc9bb 100644 --- a/Bytecode/Basic.lean +++ b/Bytecode/Basic.lean @@ -44,7 +44,6 @@ abbrev M.op (l r : M Unit) (f : Rat → Rat → Rat) : M Unit := do let r ← pop push (f l r) - def Ast.compile : Ast → M Unit | lit n => M.push n | 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, 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) : ast.compile = M.push ast.interpret := by induction ast