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

feat: add liftLevelM

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-30 09:49:04 -08:00
parent 9d577fb2d9
commit 387dbd4036
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Elab/Level.lean
View file

@ -81,5 +81,8 @@ partial def elabLevel : Syntax → LevelElabM Level
throwError stx "unexpected universe level syntax kind"
end Level
export Level (LevelElabM)
end Elab
end Lean

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

@ -11,6 +11,7 @@ import Init.Lean.Hygiene
import Init.Lean.Elab.Log
import Init.Lean.Elab.Alias
import Init.Lean.Elab.ResolveName
import Init.Lean.Elab.Level
namespace Lean
namespace Elab
@ -262,6 +263,15 @@ match u? with
| some u => pure u
| none => throwError ref ("invalid universe level, " ++ u ++ " is not greater than 0")
def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
fun ctx s =>
match (x { .. ctx }).run { .. s } with
| EStateM.Result.ok a newS => EStateM.Result.ok a { mctx := newS.mctx, ngen := newS.ngen, .. s }
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.error ex) s
def elabLevel (stx : Syntax) : TermElabM Level :=
liftLevelM $ Level.elabLevel stx
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (stx : Syntax) (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x