max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing inline

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-25 10:45:09 -07:00
parent 34acf2003c
commit 2eeeab68b3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Control/State.lean
View file

@ -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')