Zulip Chat Archive
Stream: lean4
Topic: local context without current decl
Marcus Rossel (Jan 04 2024 at 14:21):
In the following example, I'm printing the names of the declarations contained in the local context at a given point.
Apparently, the local context includes the definition currently being defined (t
in the example below).
Is there a way to reliably exclude the definition currently being defined (e.g. is it always the first element in the list)? Also, why isn't i
part of the local context in the definition of i
?
import Lean
open Lean Meta Elab Tactic
elab tk:"print_lctx" : tactic => do
withMainContext do
logInfoAt tk <| (← getLCtx).foldl (· ++ s!"{·.userName}\n") ""
theorem t (h : False) : True := by
have g : 0 = 0 := by rfl
print_lctx -- t, h, g
have i : 1 = 1 := by print_lctx; rfl -- t, h, g
print_lctx -- t, h, g, i
Kyle Miller (Jan 04 2024 at 15:32):
I think it's docs#Lean.LocalDecl.isImplementationDetail
Kyle Miller (Jan 04 2024 at 15:36):
There's also docs#Lean.LocalDecl.isAuxDecl
Kyle Miller (Jan 04 2024 at 15:37):
You can take a look one of the ppGoal routines, how it filters out local declarations: https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Lean/Meta/PPGoal.lean#L91
Last updated: May 02 2025 at 03:31 UTC