From f4f0684636feb96e866aabe36bf7bd7fec57f398 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Aug 2020 13:19:13 -0700 Subject: [PATCH] chore: remove dead code --- src/Lean/Elab/Term.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 6a40963d01..d02b03d5db 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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