Why goal in context?

Stream: lean4

[Max Nowak 🐺]

I'm a little confused why the goal is in my local context in this metaprogram:

elab "ohno" : tactic => do
  Lean.Elab.Tactic.withMainContext do
    let ctx : LocalContext <- getLCtx
    for decl in ctx do
      let expr := decl.toExpr
      let expr_t <- Meta.inferType expr
      logInfo f!"+ local decl: \"{decl.userName}\" === {expr} ::: {expr_t}"

theorem test: Nat.zero = Nat.zero := by ohno

Logs the following:

+ local decl: "test" === _uniq.4025 ::: Eq.{1} Nat Nat.zero Nat.zero

Why? I thought the local context is exactly the assumptions I can use?

[David Renshaw]

It's an auxDecl and you shouldn't use it unless you are defining something recursive. You can filter such things out by checking LocalDecl.isImplementationDetail.

[David Renshaw]

(I've been wrestling with these things recently https://github.com/leanprover-community/mathlib4/issues/1061 )