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

feat: add MonadLCtx and MonadMCtx helper classes

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-28 16:48:42 -07:00
parent 65f1c3fe65
commit 5e582823ec
2 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/LocalContext.lean
View file

@ -348,4 +348,13 @@ Id.run $ lctx.anyM p
Id.run $ lctx.allM p
end LocalContext
class MonadLCtx (m : Type → Type) :=
(getLCtx : m LocalContext)
export MonadLCtx (getLCtx)
instance monadLCtxTrans (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n :=
{ getLCtx := liftM (getLCtx : m _) }
end Lean

9
src/Lean/MetavarContext.lean
View file

@ -1049,4 +1049,13 @@ let (e, s) := LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alre
expr := e }
end MetavarContext
class MonadMCtx (m : Type → Type) :=
(getMCtx : m MetavarContext)
export MonadMCtx (getMCtx)
instance monadMCtxTrans (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n :=
{ getMCtx := liftM (getMCtx : m _) }
end Lean