Method lookup_var

crates/kernel/src/tc.rs:627–636

Look up a bound variable's type, lifted to the current depth.

(&mut self, idx: u64)

  /// 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>) {
    let name = M::meta_field(ix_common::env::Name::anon());
    let bi = M::meta_field(ix_common::env::BinderInfo::Default);
    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 });
    (fv_id, fv)
  }

  /// Look up a bound variable's type, lifted to the current depth.
  pub fn lookup_var(&mut self, idx: u64) -> Result<KExpr<M>, TcError<M>> {
    let n = self.ctx.len();
    let idx_us = u64_to_usize::<M>(idx)?;