On Lean v4.29.0, linter.unusedSimpArgs (default-on, Lean core) flags OptionT.run as an unused simp only argument in three lemmas in Loom/WP/Lemmas.lean:
tryCatch_OptionT_wp (L217): simp only [wp, MonadExceptOf.tryCatch, OptionT.tryCatch, OptionT.mk, OptionT.run]monadLift_OptionT_wp (L319): simp only [wp, MonadLift.monadLift, OptionT.mk, OptionT.lift, OptionT.run]orElse_OptionT_wp (L679): simp only [wp, OrElse.orElse, OptionT.run]
OptionT.run is a projection already discharged by the surrounding lemmas (OptionT.mk etc.), so the argument never fires. Dropping it from the three lists leaves the proofs unchanged (checked on v4.29.0).
The OptionT.run at L362 (simp only [wp, MonadFunctor.monadMap, OptionT.run]; rfl) is used and should stay.
Surfaced via the quangvdao/loom2 fork (a toolchain-only bump to v4.29.0) and downstream VCVio. The repo itself pins master, so it may not reproduce on a current Lean dev build.
On Lean
v4.29.0,linter.unusedSimpArgs(default-on, Lean core) flagsOptionT.runas an unusedsimp onlyargument in three lemmas inLoom/WP/Lemmas.lean:tryCatch_OptionT_wp(L217):simp only [wp, MonadExceptOf.tryCatch, OptionT.tryCatch, OptionT.mk, OptionT.run]monadLift_OptionT_wp(L319):simp only [wp, MonadLift.monadLift, OptionT.mk, OptionT.lift, OptionT.run]orElse_OptionT_wp(L679):simp only [wp, OrElse.orElse, OptionT.run]OptionT.runis a projection already discharged by the surrounding lemmas (OptionT.mketc.), so the argument never fires. Dropping it from the three lists leaves the proofs unchanged (checked on v4.29.0).The
OptionT.runat L362 (simp only [wp, MonadFunctor.monadMap, OptionT.run]; rfl) is used and should stay.Surfaced via the
quangvdao/loom2fork (a toolchain-only bump to v4.29.0) and downstreamVCVio. The repo itself pinsmaster, so it may not reproduce on a current Lean dev build.