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

chore: remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-26 13:19:13 -07:00
parent 5dc5e8a92f
commit f4f0684636
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Term.lean
View file

@ -270,15 +270,6 @@ let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap
def elabLevel (stx : Syntax) : TermElabM Level :=
liftLevelM $ Level.elabLevel stx
@[inline] def withConfig {α} (f : Meta.Config → Meta.Config) (x : TermElabM α) : TermElabM α :=
adaptTheReader Meta.Context (fun (ctx : Meta.Context) => { ctx with config := f ctx.config }) x
@[inline] def withTransparency {α} (mode : Meta.TransparencyMode) (x : TermElabM α) : TermElabM α :=
withConfig (fun config => { config with transparency := mode }) x
@[inline] def withReducible {α} (x : TermElabM α) : TermElabM α :=
withTransparency Meta.TransparencyMode.reducible x
/- Elaborate `x` with `stx` on the macro stack -/
@[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x