Method push_fvar_decl_anon

crates/kernel/src/tc.rs:617–624

Push a fresh fvar declaration without any body to instantiate. Useful for paths that introduce a binder for type-tracking purposes only (e.g. inductive validation walks where the binder is consumed later or in parallel). Returns the fvar id and the interned fvar expression.

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

    let fv_id = self.fresh_fvar_id();
    let fv = self.intern(KExpr::fvar(fv_id, name.clone()));
    self.lctx.push(fv_id, LocalDecl::LDecl { name, ty, val });
    let body_open = instantiate_rev(&mut self.env.intern, body, &[fv]);
    (body_open, fv_id)
  }

  /// Push a fresh fvar declaration without any body to instantiate.
  /// Useful for paths that introduce a binder for type-tracking purposes
  /// only (e.g. inductive validation walks where the binder is consumed
  /// later or in parallel). Returns the fvar id and the interned fvar
  /// expression.
  pub fn push_fvar_decl_anon(&mut self, ty: KExpr<M>) -> (FVarId, KExpr<M>) {