Method push_local

crates/kernel/src/tc.rs:448–457

Push a local variable type (lambda/forall binding, no let-value).

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

  /// Push a local variable type (lambda/forall binding, no let-value).
  /// The type is interned first: ctx suffix hashing keys on uids, so a
  /// canonical frame is what lets equal suffixes share cache entries.
  pub fn push_local(&mut self, ty: KExpr<M>) {
    let ty = self.env.intern.intern_expr(ty);
    let mut h = blake3::Hasher::new();
    h.update(b"ctx.local");
    h.update(&ty.addr().to_le_bytes());
    h.update(self.ctx_id.as_bytes());
    self.ctx_id_stack.push(self.ctx_id);
    self.ctx_id = h.finalize();
    self.ctx.push(ty);
    self.let_vals.push(None);
  }