local context without current decl

Stream: lean4

[Marcus Rossel]

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

#xy

I'm trying to get all of the hypotheses above the ⊢ in a tactic. And this shouldn't include the theorem to be proven itself.

[Kyle Miller]

I think it's docs#Lean.LocalDecl.isImplementationDetail

[Kyle Miller]

There's also docs#Lean.LocalDecl.isAuxDecl

[Kyle Miller]

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