Function syntax_like_env

crates/kernel/src/inductive.rs:5573–5773

Mimics Lean.Syntax structure: a type `Syn` that nests with `List (Pair Name Syn)` — testing multi-level transitive nesting. Syn : Sort 1 Syn.atom : Syn Syn.node : List (Pair Name Syn) → Syn This should create a flat block: [Syn, List (Pair Name Syn), Pair (Name, Syn)] with 3 motives.

()

    let count_binders = |e: &AE| -> usize {
      let mut n = 0;
      let mut c = e.clone();
      while let ExprData::All(_, _, _, b, _) = c.data() {
        n += 1;
        c = b.clone();
      }
      n
    };

    // PTree.rec: 1 param + 2 motives + 4 minors + 0 indices + 1 major = 8
    let n = count_binders(&generated[0].ty);
    assert_eq!(n, 8, "PTree.rec should have 8 binders, got {n}");
  }

  /// Mimics Lean.Syntax structure: a type `Syn` that nests with
  /// `List (Pair Name Syn)` — testing multi-level transitive nesting.
  ///
  /// Syn : Sort 1
  /// Syn.atom : Syn
  /// Syn.node : List (Pair Name Syn) → Syn
  ///
  /// This should create a flat block:
  ///   [Syn, List (Pair Name Syn), Pair (Name, Syn)]
  /// with 3 motives.
  fn syntax_like_env() -> KEnv<Anon> {
    let mut env = KEnv::new();
    let block = mk_id("Syn");
    let syn = || cnst("Syn", &[]);

    // Name : Sort 1 (axiom, external)
    env.insert(
      mk_id("Name"),
      KConst::Axio {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 0,
        ty: sort1(),
      },
    );

    // Pair.{u,v} : Sort u → Sort v → Sort (max u v)
    // Pair.mk.{u,v} : ∀ (α : Sort u) (β : Sort v), α → β → Pair.{u,v} α β
    let pair_ty = pi(
      AE::sort(param(0)),
      pi(AE::sort(param(1)), AE::sort(AU::max(param(0), param(1)))),
    );
    env.insert(
      mk_id("Pair"),
      KConst::Indc {
        name: (),
        level_params: (),
        lvls: 2,
        params: 2,
        indices: 0,
        is_unsafe: false,
        block: mk_id("Pair"),
        member_idx: 0,
        ty: pair_ty,