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

chore: missing annotations

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-15 19:51:56 -07:00
parent 9a41680ec9
commit 4b018cdc72
2 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Environment.lean
View file

@ -869,6 +869,7 @@ class MonadEnv (m : Type → Type) where
export MonadEnv (getEnv modifyEnv)
@[alwaysInline]
instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
getEnv := liftM (getEnv : m Environment)
modifyEnv := fun f => liftM (modifyEnv f : m Unit)

1
src/Lean/MetavarContext.lean
View file

@ -330,6 +330,7 @@ class MonadMCtx (m : Type → Type) where
export MonadMCtx (getMCtx modifyMCtx)
@[alwaysInline]
instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where
getMCtx := liftM (getMCtx : m _)
modifyMCtx := fun f => liftM (modifyMCtx f : m _)