chore: make Lean.Elab.Command.mkMetaContext public

leanprover · Nov 18, 2024 · f87b72c · f87b72c
1 parent ea6601e
commit f87b72c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
@@ -555,6 +555,10 @@ private def getVarDecls (s : State) : Array Syntax :=
 instance {α} : Inhabited (CommandElabM α) where
   default := throw default
 
+/--
+The environment linter framework needs to be able to run linters with the same context
+as `liftTermElabM`, so we expose that context as a public function here.
+-/
 def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
 }