Method open_binder_anon_with_fv

crates/kernel/src/tc.rs:584–592

Anonymous-name variant of [`Self::open_binder_with_fv`].

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

    ty: KExpr<M>,
    body: &KExpr<M>,
  ) -> (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, std::slice::from_ref(&fv));
    (body_open, fv, fv_id)
  }

  /// Anonymous-name variant of [`Self::open_binder_with_fv`].
  pub fn open_binder_anon_with_fv(
    &mut self,