fix MemoryEffects.validate to expect the right type

leanprover · Oct 7, 2024 · 077b5da · 077b5da
1 parent 66ad4fd
commit 077b5da
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Tactics/Sym/MemoryEffects.lean b/Tactics/Sym/MemoryEffects.lean
@@ -115,7 +115,7 @@ def validate (eff : MemoryEffects) : MetaM Unit := do
   Sym.withTraceNode msg do
     eff.traceCurrentState
     check eff.effects
-    assertHasType eff.effects mkMemory
+    assertHasType eff.effects mkArmState
 
     check eff.proof