Method lookup_let_val

crates/kernel/src/tc.rs:489–498

Look up a let-bound variable's value, lifted to the current depth. Returns None if the variable is lambda/forall-bound (not a let).

(&mut self, idx: u64)

  /// Pop the most recent local variable.
  pub fn pop_local(&mut self) {
    if let Some(Some(_)) = self.let_vals.pop() {
      self.num_let_bindings -= 1;
    }
    self.ctx.pop();
    self.ctx_id = self.ctx_id_stack.pop().unwrap_or_else(empty_ctx_addr);
  }

  /// Look up a let-bound variable's value, lifted to the current depth.
  /// Returns None if the variable is lambda/forall-bound (not a let).
  pub fn lookup_let_val(&mut self, idx: u64) -> Option<KExpr<M>> {
    let n = self.ctx.len();
    let idx_us = usize::try_from(idx).ok()?;