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

chore: helper method

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-08 17:28:31 -08:00
parent 79f30d5c8c
commit f3de32cbf4
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Elab/Term.lean
View file

@ -301,6 +301,10 @@ def getDecLevel (ref : Syntax) (type : Expr) : TermElabM Level := do
u ← getLevel ref type;
decLevel ref u
@[inline] def savingMCtx {α} (x : TermElabM α) : TermElabM α := do
mctx ← getMCtx;
finally x (modify $ fun s => { mctx := mctx, .. s })
def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
fun ctx s =>
match (x { .. ctx }).run { .. s } with