Method push_let

crates/kernel/src/tc.rs:461–472

Push a let-bound variable (type + value). WHNF will zeta-reduce references to this variable by substituting the value (lean4lean withExtendedLetCtx).

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

    self.let_vals.push(None);
  }

  /// Push a let-bound variable (type + value). WHNF will zeta-reduce references
  /// to this variable by substituting the value (lean4lean withExtendedLetCtx).
  pub fn push_let(&mut self, ty: KExpr<M>, val: KExpr<M>) {
    let ty = self.env.intern.intern_expr(ty);
    let val = self.env.intern.intern_expr(val);
    let mut h = blake3::Hasher::new();
    h.update(b"ctx.let");
    h.update(&ty.addr().to_le_bytes());
    h.update(&val.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(Some(val));