From 2eeeab68b34400faabb935bddbc1f6fec6052880 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Oct 2019 10:45:09 -0700 Subject: [PATCH] chore: missing inline --- library/Init/Control/State.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/Init/Control/State.lean b/library/Init/Control/State.lean index b85cba65d6..b3eac6b680 100644 --- a/library/Init/Control/State.lean +++ b/library/Init/Control/State.lean @@ -161,7 +161,7 @@ export MonadStateAdapter (adaptState) section variables {σ σ' : Type u} {m m' : Type u → Type v} -def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α := +@[inline] def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α := adaptState (fun st => (toSigma st, PUnit.unit)) (fun st _ => fromSigma st) export MonadStateAdapter (adaptState')