Method open_binder_anon

crates/kernel/src/tc.rs:555–563

Anonymous variant of [`Self::open_binder`] that uses `Name::anon()` / `BinderInfo::Default`. Convenient for kernel-internal walks (inductive validation, recursor synthesis) that don't carry user-visible binder metadata.

(
    &mut self,
    ty: KExpr<M>,
    body: &KExpr<M>,
  )

  ) -> (KExpr<M>, FVarId) {
    let fv_id = self.fresh_fvar_id();
    let fv = self.intern(KExpr::fvar(fv_id, name.clone()));
    self.lctx.push(fv_id, LocalDecl::CDecl { name, bi, ty });
    let body_open = instantiate_rev(&mut self.env.intern, body, &[fv]);
    (body_open, fv_id)
  }

  /// Anonymous variant of [`Self::open_binder`] that uses
  /// `Name::anon()` / `BinderInfo::Default`. Convenient for kernel-internal
  /// walks (inductive validation, recursor synthesis) that don't carry
  /// user-visible binder metadata.
  pub fn open_binder_anon(
    &mut self,