Eliminate need for forward type declarations in recursive datatypes

[joehendrix]

Summary

Mutually recursive datatypes previously required users to manually write
forward type declarations before a mutual block. This PR eliminates
that boilerplate by having the elaborator automatically discover and
pre-register type names before elaborating the block's children.

Details

• Automatic pre-registration replaces forward declarations. The
  @[preRegisterTypes(scope)] annotation on command_mutual triggers
  a two-phase elaboration: Phase 1 partially elaborates each child to
  extract type names and params, then pre-registers them in the
  GlobalContext so Phase 2 can resolve mutual references. This removes
  a common source of user confusion — forgetting or misordering forward
  declarations — and makes the mutual block self-contained.
• GlobalContext simplified. The DeclState enum
  (.forward / .defined) and its associated bookkeeping
  (declareForward, isForward, three-element vars tuples) are
  removed. Symbols are now either present or absent, tracked by a single
  ensureDefined operation. This eliminates a class of bugs where
  forward-declared symbols could be left in a half-defined state.
• O(1) argument lookup via argElabIndex. A precomputed
  Array (Option Nat) maps each argLevel to its position in
  argElaborators, replacing linear searches through
  argLevelToSyntaxLevel. Callers get the full ArgElaborator,
  not just one field.
• Translation layer adapted. Translate.lean no longer requires
  forward declarations before mutual blocks. Instead it allocates
  placeholder entries on the fly when a datatype isn't already
  pre-registered, making the AST-to-CST path work for both DDM-parsed
  and programmatically-constructed programs.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[MikaelMayer]

Clean, well-motivated PR that removes a real source of user friction. The two-phase elaboration design in elaborateWithPreRegistration is sound, the GlobalContext simplification is a clear win, and the removal of DeclState/forward declarations is thorough — no dangling references remain.

One minor inconsistency between extractParamNames and the inline code in runSyntaxElaborator (.tvar handling) is worth a look. The rest is solid.

I'd approve after the one question below is addressed.

[MikaelMayer]

extractParamNames matches both .type _ [] _ and .tvar _ _, but the analogous inline code in runSyntaxElaborator (around line 1101) only matches .type _ [] _:

|>.filterMap fun b =>
  match b.kind with
  | .type _ [] _ => some b.ident
  | _ => none

Is the .tvar case intentionally included here but not there? If both should behave the same, consider extracting the shared logic into extractParamNames and calling it from both sites.