chore: make Lean.Elab.Command.mkMetaContext public (#6113)

leanprover · Nov 18, 2024 · 5a99cb3 · 5a99cb3
1 parent e10fac9
commit 5a99cb3
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
@@ -555,7 +555,11 @@ private def getVarDecls (s : State) : Array Syntax :=
 instance {α} : Inhabited (CommandElabM α) where
   default := throw default
 
-private def mkMetaContext : Meta.Context := {
+/--
+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 }
 }