Understanding the `_example` term in the local context

Stream: lean4

[Anand Rao]

Aside from the usual variables in the local context, there always seems to be an extra variable that has the type of the main goal (this is called _example when the context is inspected in an example environment, and <def_name> when in a definition/theorem environment with name <def_name>). This is the code I used to list all the variables in a local declaration, along with their types:

syntax (name := ctxtac) "ctxtac" : tactic
@[tactic ctxtac] def ctxtacT : Tactic := fun stx => do
  for c in (← getLCtx) do
    logInfo m!"{(c.userName, c.type)}"

  let _ ← apply (← getMainGoal) (mkConst ``Unit.unit)
  return ()

example (a b : Nat) (x : List Float) : Unit := by
  ctxtac

def ctxtest (a b : Nat) (x : List Float) : Unit := by
  ctxtac

Could anyone explain what this additional variable is and why it needs to be present? Is there an easy way to erase it from the local context? Thank you in advance.

[Leonardo de Moura]

1- example <decls> := <val> is elaborated as def _example <decls> := <val>, but we discard the definition after we type check it in the kernel.
2- Definitions and theorems can be recursive, but the Lean kernel does not accept recursive definitions. Example: #print List.append shows how List.append was compiled before being sent to the kernel. Nobody wants to use List.brecOn directly. Thus, we temporarily add a local declaration for each declaration being defined. Before sending it to the kernel, we eliminate them using brecOn or WellFounded.fix. We "hide" these auxiliary declarations when printing goals.

Note that this encoding allows us to write recursive examples:

example (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n+1) * _example n

example (as : List α) : as.length ≥ 0 :=
  match as with
  | [] => Nat.le_refl _
  | a :: as => Nat.le_trans (_example as) (by simp_arith)

We can remove _example before elaborating <val> at step 1, but the recursive examples would be gone.